ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>L L₁✝ L₂✝ L₃ L₄ : List (α × Bool)<VAR>inst✝ : DecidableEq α<VAR>a₁✝ : FreeGroup α<VAR>L₁ : List (α × Bool)<VAR>a₂✝ : FreeGroup α<VAR>L₂ : List (α × Bool)<GOAL>toWord (Quot.mk Red.Step L₁) = toWord (Quot.mk Red.Step L₂) → Quot.mk Red.Step L₁ = Quot.mk Red.Step L₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : SuccOrder α<VAR>inst✝ : IsSuccArchimedean α<VAR>a b : α<GOAL>(hasse α).Reachable a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : SuccOrder α<VAR>inst✝ : IsSuccArchimedean α<VAR>a b : α<GOAL>ReflTransGen (hasse α).Adj a b
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>hn : n ≠ 0<GOAL>a ^ n < b ^ n ↔ a < b
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : Precoherent C<VAR>X : C<VAR>α : Type<VAR>inst✝¹ : Finite α<VAR>Y : α → C<VAR>π : (a : α) → Y a ⟶ X<VAR>h : EffectiveEpiFamily Y π<VAR>β : α → Type<VAR>inst✝ : ∀ (a : α), Finite (β a)<VAR>Y_n : (a : α) → β a → C<VAR>π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a<VAR>H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)<GOAL>EffectiveEpiFamily (fun c => Y_n c.fst c.snd) fun c => π_n c.fst c.snd ≫ π c.fst
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : Precoherent C<VAR>X : C<VAR>α : Type<VAR>inst✝¹ : Finite α<VAR>Y : α → C<VAR>π : (a : α) → Y a ⟶ X<VAR>h : EffectiveEpiFamily Y π<VAR>β : α → Type<VAR>inst✝ : ∀ (a : α), Finite (β a)<VAR>Y_n : (a : α) → β a → C<VAR>π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a<VAR>H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)<GOAL>(Presieve.ofArrows (fun c => Y_n c.fst c.snd) fun c => π_n c.fst c.snd ≫ π c.fst).EffectiveEpimorphic
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : Precoherent C<VAR>X : C<VAR>α : Type<VAR>inst✝¹ : Finite α<VAR>Y : α → C<VAR>π : (a : α) → Y a ⟶ X<VAR>h : EffectiveEpiFamily Y π<VAR>β : α → Type<VAR>inst✝ : ∀ (a : α), Finite (β a)<VAR>Y_n : (a : α) → β a → C<VAR>π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a<VAR>H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)<GOAL>Sieve.generate (Presieve.ofArrows (fun x => match x with | ⟨a, b⟩ => Y_n a b) fun x => match x with | ⟨a, b⟩ => π_n a b ≫ π a) ∈ (coherentTopology C).sieves X
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<GOAL>↑2⁻¹ = 2⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>s : ι → Set α<VAR>t : α → Set β<GOAL>⋂ x ∈ ⋃ i, s i, t x = ⋂ i, ⋂ x ∈ s i, t x
<VAR>R : Type u<VAR>inst✝¹⁴ : CommSemiring R<VAR>S : Type u_1<VAR>inst✝¹³ : Semiring S<VAR>inst✝¹² : Algebra R S<VAR>ι₁ : Type v₁<VAR>ι₂ : Type v₂<VAR>inst✝¹¹ : DecidableEq ι₁<VAR>inst✝¹⁰ : DecidableEq ι₂<VAR>M₁ : ι₁ → Type w₁<VAR>M₁' : Type w₁'<VAR>M₂ : ι₂ → Type w₂<VAR>M₂' : Type w₂'<VAR>inst✝⁹ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)<VAR>inst✝⁸ : AddCommMonoid M₁'<VAR>inst✝⁷ : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)<VAR>inst✝⁶ : AddCommMonoid M₂'<VAR>inst✝⁵ : (i₁ : ι₁) → Module R (M₁ i₁)<VAR>inst✝⁴ : Module R M₁'<VAR>inst✝³ : (i₂ : ι₂) → Module R (M₂ i₂)<VAR>inst✝² : Module R M₂'<VAR>inst✝¹ : (i₁ : ι₁) → Module S (M₁ i₁)<VAR>inst✝ : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)<VAR>i₁ : ι₁<VAR>m₁ : M₁ i₁<VAR>i₂ : ι₂<VAR>m₂ : M₂ i₂<GOAL>(TensorProduct.directSum R S M₁ M₂).symm ((lof S (ι₁ × ι₂) (fun i => M₁ i.1 ⊗[R] M₂ i.2) (i₁, i₂)) (m₁ ⊗ₜ[R] m₂)) = (lof S ι₁ M₁ i₁) m₁ ⊗ₜ[R] (lof R ι₂ M₂ i₂) m₂
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>inst✝² : Category.{u_3, u_1} J<VAR>inst✝¹ : Category.{u_4, u_2} C<VAR>inst✝ : ChosenFiniteProducts C<VAR>F : J ⥤ C<VAR>j : J<GOAL>(ρ_ F).inv.app j = (ρ_ (F.obj j)).inv
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>mδ : MeasurableSpace δ<VAR>f : β → γ<VAR>g : γ → α<VAR>κ : Kernel α β<VAR>inst✝ : IsSFiniteKernel κ<VAR>hg : Measurable g<VAR>a : γ<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>((Kernel.sum fun n => (κ.seq n).comap g hg) a) s = ((κ.comap g hg) a) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>mδ : MeasurableSpace δ<VAR>f : β → γ<VAR>g : γ → α<VAR>κ : Kernel α β<VAR>inst✝ : IsSFiniteKernel κ<VAR>hg : Measurable g<VAR>a : γ<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>∑' (i : ℕ), (((κ.seq i).comap g hg) a) s = ∑' (i : ℕ), ((κ.seq i) (g a)) s
<VAR>x : ℂ<VAR>n : ℕ<VAR>h₀ : n ≠ 0<VAR>hlt : -(π / ↑n) < x.arg<VAR>hle : x.arg ≤ π / ↑n<GOAL>(x ^ n) ^ (↑n)⁻¹ = x
<VAR>x : ℂ<VAR>n : ℕ<VAR>h₀ : n ≠ 0<VAR>hlt : -(π / ↑n) < x.arg<VAR>hle : x.arg ≤ π / ↑n<GOAL>-π < ↑n * x.arg
<VAR>x : ℂ<VAR>n : ℕ<VAR>h₀ : n ≠ 0<VAR>hlt : -(π / ↑n) < x.arg<VAR>hle : x.arg ≤ π / ↑n<GOAL>↑n * x.arg ≤ π
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : MonoidalCategory D<VAR>inst✝ : BraidedCategory D<VAR>F : C ⥤ CommMon_ D<VAR>X : C<GOAL>((β_ __src✝.X __src✝.X).hom ≫ __src✝.mul).app X = __src✝.mul.app X
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>inst✝¹ : Semiring α<VAR>inst✝ : Semiring β<VAR>a b : α<VAR>m n : ℕ<GOAL>Odd (a + 1 + a)
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>H : Subgroup G<VAR>A : Type u_2<VAR>inst✝¹ : CommGroup A<VAR>ϕ : ↥H →* A<VAR>R S T : ↑(leftTransversals ↑H)<VAR>inst✝ : H.FiniteIndex<VAR>q : G ⧸ H<VAR>x✝ : q ∈ univ<GOAL>⟨(↑((MemLeftTransversals.toEquiv ⋯) q))⁻¹ * ↑((MemLeftTransversals.toEquiv ⋯) q), ⋯⟩ * ⟨(↑((MemLeftTransversals.toEquiv ⋯) q))⁻¹ * ↑((MemLeftTransversals.toEquiv ⋯) q), ⋯⟩ = ⟨(↑((MemLeftTransversals.toEquiv ⋯) q))⁻¹ * ↑((MemLeftTransversals.toEquiv ⋯) q), ⋯⟩
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → α<VAR>m : ℕ<GOAL>f^[m * 0] = f^[m]^[0]
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → α<VAR>m n : ℕ<GOAL>f^[m * (n + 1)] = f^[m]^[n + 1]
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>s : l₁ ~ l₂<VAR>p p' : α → Bool<VAR>hp : ∀ (x : α), x ∈ l₁ → p x = p' x<GOAL>countP p l₁ = countP p' l₂
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>s : l₁ ~ l₂<VAR>p p' : α → Bool<VAR>hp : ∀ (x : α), x ∈ l₁ → p x = p' x<GOAL>countP p l₁ = countP p' l₁
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>p p' : α → Bool<VAR>hp : ∀ (x : α), x ∈ l₁ → p x = p' x<GOAL>countP p l₁ = countP p' l₁
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>r s : R<VAR>ε : ℚ<VAR>hε : ε > 0<GOAL>∃ i, ∀ j ≥ i, padicNorm p (↑(nthHomSeq f_compat (r + s) - (nthHomSeq f_compat r + nthHomSeq f_compat s)) j) < ε
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>r s : R<VAR>ε : ℚ<VAR>hε : ε > 0<VAR>n : ℕ<VAR>hn : ↑p ^ (-↑n) < ε<GOAL>∃ i, ∀ j ≥ i, padicNorm p (↑(nthHomSeq f_compat (r + s) - (nthHomSeq f_compat r + nthHomSeq f_compat s)) j) < ε
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>r s : R<VAR>ε : ℚ<VAR>hε : ε > 0<VAR>n : ℕ<VAR>hn : ↑p ^ (-↑n) < ε<GOAL>∀ j ≥ n, padicNorm p (↑(nthHomSeq f_compat (r + s) - (nthHomSeq f_compat r + nthHomSeq f_compat s)) j) < ε
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>r s : R<VAR>ε : ℚ<VAR>hε : ε > 0<VAR>n : ℕ<VAR>hn : ↑p ^ (-↑n) < ε<VAR>j : ℕ<VAR>hj : j ≥ n<GOAL>padicNorm p (↑(nthHom f (r + s) j) - (↑(nthHom f r j) + ↑(nthHom f s j))) < ε
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>r s : R<VAR>ε : ℚ<VAR>hε : ε > 0<VAR>n : ℕ<VAR>hn : ↑p ^ (-↑n) < ε<VAR>j : ℕ<VAR>hj : j ≥ n<GOAL>padicNorm p (↑(nthHom f (r + s) j) - (↑(nthHom f r j) + ↑(nthHom f s j))) ≤ ↑p ^ (-↑n)
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>r s : R<VAR>ε : ℚ<VAR>hε : ε > 0<VAR>n : ℕ<VAR>hn : ↑p ^ (-↑n) < ε<VAR>j : ℕ<VAR>hj : j ≥ n<GOAL>↑(nthHom f (r + s) j - (nthHom f r j + nthHom f s j)) = 0
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>r s : R<VAR>ε : ℚ<VAR>hε : ε > 0<VAR>n : ℕ<VAR>hn : ↑p ^ (-↑n) < ε<VAR>j : ℕ<VAR>hj : j ≥ n<GOAL>↑(↑((f j) (r + s)).val - (↑((f j) r).val + ↑((f j) s).val)) = 0
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>r s : R<VAR>ε : ℚ<VAR>hε : ε > 0<VAR>n : ℕ<VAR>hn : ↑p ^ (-↑n) < ε<VAR>j : ℕ<VAR>hj : j ≥ n<GOAL>((f j) r + (f j) s).cast - (((f j) r).cast + ((f j) s).cast) = 0
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>r s : R<VAR>ε : ℚ<VAR>hε : ε > 0<VAR>n : ℕ<VAR>hn : ↑p ^ (-↑n) < ε<VAR>j : ℕ<VAR>hj : j ≥ n<GOAL>((f j) r).cast + ((f j) s).cast - (((f j) r).cast + ((f j) s).cast) = 0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : Module.Free R M<VAR>inst✝ : Module.Finite R M<VAR>x y : L<VAR>hx : x ∈ lowerCentralSeries R L L 1<VAR>hy : y ∈ LieAlgebra.center R L<GOAL>((traceForm R L M) x) y = 0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : Module.Free R M<VAR>inst✝ : Module.Finite R M<VAR>x y : L<VAR>hx : x ∈ lowerCentralSeries R L L 1<VAR>hy : y ∈ LieAlgebra.center R L<GOAL>x ∈ ⊤.lcs L 1
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : Module.Free R M<VAR>inst✝ : Module.Finite R M<VAR>x y : L<VAR>hx : x ∈ lowerCentralSeries R L L 1<VAR>hy : y ∈ LieAlgebra.center R L<GOAL>y ∈ LieSubmodule.ucs 1 ⊥
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : IsDomain R<VAR>inst✝⁷ : CommRing S<VAR>L : Type u_3<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Algebra S L<VAR>inst✝³ : Algebra R L<VAR>inst✝² : IsScalarTower R S L<VAR>inst✝¹ : IsIntegralClosure S R L<VAR>inst✝ : Algebra.IsAlgebraic R L<VAR>inj : Function.Injective ⇑(algebraMap R L)<VAR>a b : S<VAR>hb : b ≠ 0<GOAL>∃ c d, d ≠ 0 ∧ d • a = b * c
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : IsDomain R<VAR>inst✝⁷ : CommRing S<VAR>L : Type u_3<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Algebra S L<VAR>inst✝³ : Algebra R L<VAR>inst✝² : IsScalarTower R S L<VAR>inst✝¹ : IsIntegralClosure S R L<VAR>inst✝ : Algebra.IsAlgebraic R L<VAR>inj : Function.Injective ⇑(algebraMap R L)<VAR>a b : S<VAR>hb : b ≠ 0<VAR>c : ↥(integralClosure R L)<VAR>d : R<VAR>d_ne : d ≠ 0<VAR>hx : (algebraMap S L) a / (algebraMap S L) b * (algebraMap R L) d = ↑c<GOAL>∃ c d, d ≠ 0 ∧ d • a = b * c
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : IsDomain R<VAR>inst✝⁷ : CommRing S<VAR>L : Type u_3<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Algebra S L<VAR>inst✝³ : Algebra R L<VAR>inst✝² : IsScalarTower R S L<VAR>inst✝¹ : IsIntegralClosure S R L<VAR>inst✝ : Algebra.IsAlgebraic R L<VAR>inj : Function.Injective ⇑(algebraMap R L)<VAR>a b : S<VAR>hb : b ≠ 0<VAR>c : ↥(integralClosure R L)<VAR>d : R<VAR>d_ne : d ≠ 0<VAR>hx : (algebraMap S L) a / (algebraMap S L) b * (algebraMap R L) d = ↑c<GOAL>(algebraMap S L) (d • a) = (algebraMap S L) (b * mk' S ↑c ⋯)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : IsDomain R<VAR>inst✝⁷ : CommRing S<VAR>L : Type u_3<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Algebra S L<VAR>inst✝³ : Algebra R L<VAR>inst✝² : IsScalarTower R S L<VAR>inst✝¹ : IsIntegralClosure S R L<VAR>inst✝ : Algebra.IsAlgebraic R L<VAR>inj : Function.Injective ⇑(algebraMap R L)<VAR>a b : S<VAR>hb : b ≠ 0<VAR>c : ↥(integralClosure R L)<VAR>d : R<VAR>d_ne : d ≠ 0<VAR>hx : (algebraMap S L) a / (algebraMap S L) b * (algebraMap R L) d = ↑c<GOAL>(algebraMap R L) d * (algebraMap S L) a = (algebraMap S L) b * ((algebraMap S L) a / (algebraMap S L) b * (algebraMap R L) d)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : IsDomain R<VAR>inst✝⁷ : CommRing S<VAR>L : Type u_3<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Algebra S L<VAR>inst✝³ : Algebra R L<VAR>inst✝² : IsScalarTower R S L<VAR>inst✝¹ : IsIntegralClosure S R L<VAR>inst✝ : Algebra.IsAlgebraic R L<VAR>inj : Function.Injective ⇑(algebraMap R L)<VAR>a b : S<VAR>hb : b ≠ 0<VAR>c : ↥(integralClosure R L)<VAR>d : R<VAR>d_ne : d ≠ 0<VAR>hx : (algebraMap S L) a / (algebraMap S L) b * (algebraMap R L) d = ↑c<GOAL>(algebraMap S L) b ≠ 0
<VAR>α : Type u_1<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>S : Set α<VAR>hS : BooleanGenerators S<VAR>h : sSup S = ⊤<VAR>a : α<GOAL>∃ s, a = sSup s ∧ ∀ a ∈ s, IsAtom a
<VAR>α : Type u_1<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>S : Set α<VAR>hS : BooleanGenerators S<VAR>h : sSup S = ⊤<VAR>a : α<VAR>s : Set α<VAR>hs : s ⊆ S<VAR>hs' : a = sSup s<GOAL>∃ s, a = sSup s ∧ ∀ a ∈ s, IsAtom a
<VAR>α : Type u<VAR>L L₁ L₂ L₃ L₄ : List (α × Bool)<VAR>x1 : α<VAR>b1 : Bool<VAR>x2 : α<VAR>b2 : Bool<VAR>H1 : (x1, b1) ≠ (x2, b2)<VAR>H2 : Red ((x1, b1) :: L₁) ((x2, b2) :: L₂)<VAR>this : Red ((x1, b1) :: L₁) ([(x2, b2)] ++ L₂)<GOAL>Red L₁ ((x1, !b1) :: (x2, b2) :: L₂)
<VAR>α : Type u<VAR>L L₁ L₂ L₃ L₄✝ : List (α × Bool)<VAR>x1 : α<VAR>b1 : Bool<VAR>x2 : α<VAR>b2 : Bool<VAR>H1 : (x1, b1) ≠ (x2, b2)<VAR>H2 : Red ((x1, b1) :: L₁) ((x2, b2) :: L₂)<VAR>this : Red ((x1, b1) :: L₁) ([(x2, b2)] ++ L₂)<VAR>L₄ : List (α × Bool)<VAR>eq : (x1, b1) :: L₁ = [] ++ L₄<VAR>h₁ : Red [] [(x2, b2)]<VAR>h₂ : Red L₄ L₂<GOAL>Red L₁ ((x1, !b1) :: (x2, b2) :: L₂)
<VAR>α : Type u<VAR>L L₁ L₂ L₃✝ L₄✝ : List (α × Bool)<VAR>x1 : α<VAR>b1 : Bool<VAR>x2 : α<VAR>b2 : Bool<VAR>H1 : (x1, b1) ≠ (x2, b2)<VAR>H2 : Red ((x1, b1) :: L₁) ((x2, b2) :: L₂)<VAR>this : Red ((x1, b1) :: L₁) ([(x2, b2)] ++ L₂)<VAR>p : α × Bool<VAR>L₃ L₄ : List (α × Bool)<VAR>eq : (x1, b1) :: L₁ = p :: L₃ ++ L₄<VAR>h₁ : Red (p :: L₃) [(x2, b2)]<VAR>h₂ : Red L₄ L₂<GOAL>Red L₁ ((x1, !b1) :: (x2, b2) :: L₂)
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : DecidableEq α<VAR>f : Perm α<VAR>x y : α<GOAL>swap (f x) (f y) = f * swap x y * f⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ ν μ : Measure α<VAR>inst✝¹ : IsFiniteMeasure ν<VAR>inst✝ : ν.HaveLebesgueDecomposition μ<VAR>r : ℝ≥0<VAR>hr : r ≠ 0<GOAL>ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ ν μ : Measure α<VAR>inst✝¹ : IsFiniteMeasure ν<VAR>inst✝ : ν.HaveLebesgueDecomposition μ<VAR>r : ℝ≥0<VAR>hr : r ≠ 0<GOAL>ν.rnDeriv (r • μ) =ᶠ[ae (r • μ)] r⁻¹ • ν.rnDeriv μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ ν μ : Measure α<VAR>inst✝¹ : IsFiniteMeasure ν<VAR>inst✝ : ν.HaveLebesgueDecomposition μ<VAR>r : ℝ≥0<VAR>hr : r ≠ 0<GOAL>(r • μ).withDensity (ν.rnDeriv (r • μ)) = (r • μ).withDensity (r⁻¹ • ν.rnDeriv μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ ν μ : Measure α<VAR>inst✝¹ : IsFiniteMeasure ν<VAR>inst✝ : ν.HaveLebesgueDecomposition μ<VAR>r : ℝ≥0<VAR>hr : r ≠ 0<GOAL>AEMeasurable (ν.rnDeriv (r • μ)) (r • μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ ν μ : Measure α<VAR>inst✝¹ : IsFiniteMeasure ν<VAR>inst✝ : ν.HaveLebesgueDecomposition μ<VAR>r : ℝ≥0<VAR>hr : r ≠ 0<GOAL>AEMeasurable (r⁻¹ • ν.rnDeriv μ) (r • μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ ν μ : Measure α<VAR>inst✝¹ : IsFiniteMeasure ν<VAR>inst✝ : ν.HaveLebesgueDecomposition μ<VAR>r : ℝ≥0<VAR>hr : r ≠ 0<GOAL>∫⁻ (x : α), ν.rnDeriv (r • μ) x ∂r • μ ≠ ⊤
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝¹ : Category.{?u.13153, u_1} D<VAR>P : MorphismProperty C<VAR>inst✝ : P.RespectsIso<VAR>f g : Arrow C<VAR>e : f ≅ g<GOAL>P f.hom ↔ P g.hom
<VAR>α : Type u_1<VAR>A : Set α<VAR>β : Type u_2<VAR>inst✝¹ : Zero β<VAR>inst✝ : TopologicalSpace β<VAR>ι : Type u_3<VAR>L : Filter ι<VAR>As : ι → Set α<VAR>b : β<VAR>nhd_b : {0}ᶜ ∈ 𝓝 b<VAR>nhd_o : {b}ᶜ ∈ 𝓝 0<GOAL>Tendsto (fun i => (As i).indicator fun x => b) L (𝓝 (A.indicator fun x => b)) ↔ Tendsto As L (pi fun x => pure (x ∈ A))
<VAR>α : Type u_1<VAR>A : Set α<VAR>β : Type u_2<VAR>inst✝¹ : Zero β<VAR>inst✝ : TopologicalSpace β<VAR>ι : Type u_3<VAR>L : Filter ι<VAR>As : ι → Set α<VAR>b : β<VAR>nhd_b : {0}ᶜ ∈ 𝓝 b<VAR>nhd_o : {b}ᶜ ∈ 𝓝 0<GOAL>(∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) ↔ ∀ (i : α), Tendsto (fun x => As x i) L (pure (i ∈ A))
<VAR>α : Type u_1<VAR>A : Set α<VAR>β : Type u_2<VAR>inst✝¹ : Zero β<VAR>inst✝ : TopologicalSpace β<VAR>ι : Type u_3<VAR>L : Filter ι<VAR>As : ι → Set α<VAR>b : β<VAR>nhd_b : {0}ᶜ ∈ 𝓝 b<VAR>nhd_o : {b}ᶜ ∈ 𝓝 0<GOAL>(∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) ↔ ∀ (i : α), ∀ᶠ (x : ι) in L, As x i = (i ∈ A)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>B : Set X<GOAL>IsBlock G B ↔ ∀ (g : G), g • B ∩ B ≠ ∅ → g • B = B
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : BorelSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : BorelSpace β<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>f : δ → α<VAR>hf : ∀ (x : α), MeasurableSet (f ⁻¹' Iio x)<GOAL>Measurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : BorelSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : BorelSpace β<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>f : δ → α<VAR>hf : ∀ (x : α), MeasurableSet (f ⁻¹' Iio x)<GOAL>inst✝⁸ = MeasurableSpace.generateFrom ?convert_2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : BorelSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : BorelSpace β<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>f : δ → α<VAR>hf : ∀ (x : α), MeasurableSet (f ⁻¹' Iio x)<GOAL>Set (Set α)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : BorelSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : BorelSpace β<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>f : δ → α<VAR>hf : ∀ (x : α), MeasurableSet (f ⁻¹' Iio x)<GOAL>∀ t ∈ ?convert_2, MeasurableSet (f ⁻¹' t)
<VAR>α : Type u_1<VAR>G₀ : Type u_2<VAR>inst✝¹ : CommGroupWithZero G₀<VAR>inst✝ : DecidableEq G₀<VAR>a : G₀<VAR>h0 : a ≠ 0<GOAL>normalize a = 1
<VAR>x : ℝ<GOAL>sin (π / 3) ^ 2 = 3 / 4
<VAR>x : ℝ<GOAL>cos (π / 2 - π / 3) ^ 2 = cos (π / 6) ^ 2
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>ε : Type u_4<VAR>f : α → β → γ<VAR>l : List α<VAR>l' : List β<VAR>i : ℕ<VAR>h : i < (zipWith f l l').length<GOAL>(zipWith f l l')[i] = f l[i] l'[i]
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>ε : Type u_4<VAR>f : α → β → γ<VAR>l : List α<VAR>l' : List β<VAR>i : ℕ<VAR>h : i < (zipWith f l l').length<GOAL>∃ x y, l[i]? = some x ∧ l'[i]? = some y ∧ f x y = f l[i] l'[i]
<VAR>x y : ℝ<VAR>hx : x < 0<GOAL>rexp (log x) = -x
<VAR>x y : ℝ<VAR>hx : x < 0<GOAL>|x| = -x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l✝ l₁ l₂ : List α<VAR>a : α<VAR>l : List α<VAR>f g : α → List β<VAR>h : ∀ a ∈ l, f a ~ g a<GOAL>Forall₂ (fun x x_1 => x ~ x_1) (List.map f l) (List.map g l)
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>g : α → β<VAR>f : α → α<VAR>a : α<GOAL>corec g f a = g a :: corec g f (f a)
<VAR>α : Type u_1<VAR>xs : List α<VAR>p : α → Bool<VAR>w : findIdx? p xs = none<VAR>i : Nat<GOAL>match xs.get? i with | some a => ¬p a = true | none => true = true
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : OrderTopology α<VAR>a : α<GOAL>𝓝 a = (⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : OrderTopology α<VAR>a : α<GOAL>⨅ s ∈ {s | a ∈ s ∧ s ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a}}, 𝓟 s = (⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b)
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Module R M<VAR>N : Submodule R M<VAR>ϕ : M →ₗ[R] R<VAR>inst✝ : (map ϕ N).IsPrincipal<VAR>x : M<VAR>hx : x ∈ N<GOAL>generator (map ϕ N) ∣ ϕ x
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Module R M<VAR>N : Submodule R M<VAR>ϕ : M →ₗ[R] R<VAR>inst✝ : (map ϕ N).IsPrincipal<VAR>x : M<VAR>hx : x ∈ N<GOAL>∃ y ∈ N, ϕ y = ϕ x
<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>γ : (a : α) → β a → Type u_7<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : (a : α) → DecidableEq (β a)<VAR>f : (i : (a : α) × β a) → γ i.fst i.snd<VAR>ia : α<VAR>ib : β ia<VAR>x : γ ⟨ia, ib⟩.fst ⟨ia, ib⟩.snd<VAR>ja : α<VAR>jb : β ja<GOAL>update f ⟨ia, ib⟩ x ⟨ja, jb⟩ = update (fun x y => f ⟨x, y⟩) ⟨ia, ib⟩.fst (update (fun y => f ⟨⟨ia, ib⟩.fst, y⟩) ⟨ia, ib⟩.snd x) ja jb
<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>γ : (a : α) → β a → Type u_7<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : (a : α) → DecidableEq (β a)<VAR>f : (i : (a : α) × β a) → γ i.fst i.snd<VAR>ia : α<VAR>ib : β ia<VAR>x : γ ⟨ia, ib⟩.fst ⟨ia, ib⟩.snd<VAR>jb : β ia<GOAL>update f ⟨ia, ib⟩ x ⟨ia, jb⟩ = update (fun x y => f ⟨x, y⟩) ⟨ia, ib⟩.fst (update (fun y => f ⟨⟨ia, ib⟩.fst, y⟩) ⟨ia, ib⟩.snd x) ia jb
<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>γ : (a : α) → β a → Type u_7<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : (a : α) → DecidableEq (β a)<VAR>f : (i : (a : α) × β a) → γ i.fst i.snd<VAR>ia : α<VAR>ib : β ia<VAR>x : γ ⟨ia, ib⟩.fst ⟨ia, ib⟩.snd<VAR>ja : α<VAR>jb : β ja<VAR>ha : ia ≠ ja<GOAL>update f ⟨ia, ib⟩ x ⟨ja, jb⟩ = update (fun x y => f ⟨x, y⟩) ⟨ia, ib⟩.fst (update (fun y => f ⟨⟨ia, ib⟩.fst, y⟩) ⟨ia, ib⟩.snd x) ja jb
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : (i : ι) → CanonicallyLinearOrderedAddCommMonoid (α i)<VAR>inst✝ : DecidableEq ι<VAR>f g : Π₀ (i : ι), α i<GOAL>Disjoint f g ↔ Disjoint f.support g.support