ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>g : β → M<VAR>e : α → β<VAR>he₀ : Function.Bijective e<VAR>he₁ : ∀ (x : α), f x = g (e x)<GOAL>∑ᶠ (i : α), f i = ∑ᶠ (j : β), g j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>g : β → M<VAR>e : α → β<VAR>he₀ : Function.Bijective e<GOAL>∑ᶠ (i : α), g (e i) = ∑ᶠ (j : β), g j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>CommMonoid M<VAR>g : β → M<VAR>e : α → β<VAR>he₀ : Function.Bijective e<GOAL>∏ᶠ (i : α), g (e i) = ∏ᶠ (j : β), g j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>CommMonoid M<VAR>e : α ≃ β<VAR>f : β → M<GOAL>∏ᶠ (i : α), f (e i) = ∏ᶠ (i' : β), f i'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>e : α ≃ β<VAR>f : β → M<GOAL>∑ᶠ (i : α), f (e i) = ∑ᶠ (i' : β), f i'
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>s : Set α<GOAL>∑ᶠ (j : ↑s), f ↑j = ∑ᶠ (i : α) (_ : i ∈ s), f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>s : Set α<GOAL>∏ᶠ (j : ↑s), f ↑j = ∏ᶠ (i : α) (_ : i ∈ s), f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>p : α → Prop<GOAL>∏ᶠ (j : Subtype p), f ↑j = ∏ᶠ (i : α) (_ : p i), f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>p : α → Prop<GOAL>∑ᶠ (j : Subtype p), f ↑j = ∑ᶠ (i : α) (_ : p i), f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>s : Set α<VAR>t : Set α<VAR>h : (s ∩ Function.support f).Finite<GOAL>∑ᶠ (i : α) (_ : i ∈ s ∩ t), f i + ∑ᶠ (i : α) (_ : i ∈ s \ t), f i = ∑ᶠ (i : α) (_ : i ∈ s), f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>s : Set α<VAR>t : Set α<VAR>h : (s ∩ Function.mulSupport f).Finite<GOAL>(∏ᶠ (i : α) (_ : i ∈ s ∩ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s \ t), f i = ∏ᶠ (i : α) (_ : i ∈ s), f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>s : Set α<VAR>t : Set α<VAR>h : s.Finite<GOAL>∑ᶠ (i : α) (_ : i ∈ s ∩ t), f i + ∑ᶠ (i : α) (_ : i ∈ s \ t), f i = ∑ᶠ (i : α) (_ : i ∈ s), f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>s : Set α<VAR>t : Set α<VAR>h : s.Finite<GOAL>(∏ᶠ (i : α) (_ : i ∈ s ∩ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s \ t), f i = ∏ᶠ (i : α) (_ : i ∈ s), f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>s t : Set α<VAR>hst : s ⊆ t<VAR>ht : (t ∩ Function.support f).Finite<GOAL>∑ᶠ (i : α) (_ : i ∈ s), f i + ∑ᶠ (i : α) (_ : i ∈ t \ s), f i = ∑ᶠ (i : α) (_ : i ∈ t), f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>s t : Set α<VAR>hst : s ⊆ t<VAR>ht : (t ∩ Function.mulSupport f).Finite<GOAL>(∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ t \ s), f i = ∏ᶠ (i : α) (_ : i ∈ t), f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>s t : Set α<VAR>hst : s ⊆ t<VAR>ht : t.Finite<GOAL>∑ᶠ (i : α) (_ : i ∈ s), f i + ∑ᶠ (i : α) (_ : i ∈ t \ s), f i = ∑ᶠ (i : α) (_ : i ∈ t), f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>s t : Set α<VAR>hst : s ⊆ t<VAR>ht : t.Finite<GOAL>(∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ t \ s), f i = ∏ᶠ (i : α) (_ : i ∈ t), f i
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>Finite ι<VAR>t : ι → Set α<VAR>h : Pairwise (Disjoint on t)<VAR>ht : ∀ (i : ι), (t i).Finite<GOAL>∏ᶠ (a : α) (_ : a ∈ ⋃ i, t i), f a = ∏ᶠ (i : ι) (a : α) (_ : a ∈ t i), f a
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>Finite ι<VAR>t : ι → Set α<VAR>h : Pairwise (Disjoint on t)<VAR>ht : ∀ (i : ι), (t i).Finite<GOAL>∑ᶠ (a : α) (_ : a ∈ ⋃ i, t i), f a = ∑ᶠ (i : ι) (a : α) (_ : a ∈ t i), f a
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>I : Set ι<VAR>t : ι → Set α<VAR>h : I.PairwiseDisjoint t<VAR>hI : I.Finite<VAR>ht : ∀ i ∈ I, (t i).Finite<GOAL>∏ᶠ (a : α) (_ : a ∈ ⋃ x ∈ I, t x), f a = ∏ᶠ (i : ι) (_ : i ∈ I) (j : α) (_ : j ∈ t i), f j
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>I : Set ι<VAR>t : ι → Set α<VAR>h : I.PairwiseDisjoint t<VAR>hI : I.Finite<VAR>ht : ∀ i ∈ I, (t i).Finite<GOAL>∑ᶠ (a : α) (_ : a ∈ ⋃ x ∈ I, t x), f a = ∑ᶠ (i : ι) (_ : i ∈ I) (j : α) (_ : j ∈ t i), f j
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>t : Set (Set α)<VAR>h : t.PairwiseDisjoint id<VAR>ht₀ : t.Finite<VAR>ht₁ : ∀ x ∈ t, x.Finite<GOAL>∏ᶠ (a : α) (_ : a ∈ ⋃₀ t), f a = ∏ᶠ (s : Set α) (_ : s ∈ t) (a : α) (_ : a ∈ s), f a
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>t : Set (Set α)<VAR>h : t.PairwiseDisjoint id<VAR>ht₀ : t.Finite<VAR>ht₁ : ∀ x ∈ t, x.Finite<GOAL>∑ᶠ (a : α) (_ : a ∈ ⋃₀ t), f a = ∑ᶠ (s : Set α) (_ : s ∈ t) (a : α) (_ : a ∈ s), f a
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>a : α<VAR>hf : (Function.mulSupport f).Finite<GOAL>f a * ∏ᶠ (i : α) (_ : i ≠ a), f i = ∏ᶠ (i : α), f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>a : α<VAR>hf : (Function.support f).Finite<GOAL>f a + ∑ᶠ (i : α) (_ : i ≠ a), f i = ∑ᶠ (i : α), f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β → M<VAR>hs : s.Finite<VAR>ht : t.Finite<GOAL>∑ᶠ (i : α) (_ : i ∈ s) (j : β) (_ : j ∈ t), f i j = ∑ᶠ (j : β) (_ : j ∈ t) (i : α) (_ : i ∈ s), f i j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>CommMonoid M<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β → M<VAR>hs : s.Finite<VAR>ht : t.Finite<GOAL>∏ᶠ (i : α) (_ : i ∈ s) (j : β) (_ : j ∈ t), f i j = ∏ᶠ (j : β) (_ : j ∈ t) (i : α) (_ : i ∈ s), f i j
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>s : Set α<VAR>p : M → Prop<VAR>hp₀ : p 0<VAR>hp₁ : ∀ (x y : M), p x → p y → p (x + y)<VAR>hp₂ : ∀ x ∈ s, p (f x)<GOAL>p (∑ᶠ (i : α) (_ : i ∈ s), f i)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>s : Set α<VAR>p : M → Prop<VAR>hp₀ : p 1<VAR>hp₁ : ∀ (x y : M), p x → p y → p (x * y)<VAR>hp₂ : ∀ x ∈ s, p (f x)<GOAL>p (∏ᶠ (i : α) (_ : i ∈ s), f i)
<VAR>α : Type u_1<VAR>R : Type u_7<VAR>OrderedCommSemiring R<VAR>p : α → Prop<VAR>f : α → R<VAR>hf : ∀ (x : α), p x → 0 ≤ f x<GOAL>0 ≤ ∏ᶠ (x : α) (_ : p x), f x
<VAR>α : Type u_1<VAR>M : Type u_7<VAR>OrderedAddCommMonoid M<VAR>i : α<VAR>f : α → M<VAR>hf : (Function.support f).Finite<VAR>h : ∀ (j : α), 0 ≤ f j<GOAL>f i ≤ ∑ᶠ (j : α), f j
<VAR>α : Type u_1<VAR>M : Type u_7<VAR>OrderedCommMonoid M<VAR>i : α<VAR>f : α → M<VAR>hf : (Function.mulSupport f).Finite<VAR>h : ∀ (j : α), 1 ≤ f j<GOAL>f i ≤ ∏ᶠ (j : α), f j
<VAR>α : Type u_1<VAR>M₀ : Type u_7<VAR>CommMonoidWithZero M₀<VAR>f : α → M₀<VAR>x : α<VAR>hx : f x = 0<VAR>hf : (Function.mulSupport f).Finite<GOAL>∏ᶠ (x : α), f x = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>s : Finset β<VAR>f : α → β → M<VAR>h : ∀ b ∈ s, (Function.support fun a => f a b).Finite<GOAL>∑ᶠ (a : α), ∑ b ∈ s, f a b = ∑ b ∈ s, ∑ᶠ (a : α), f a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>CommMonoid M<VAR>s : Finset β<VAR>f : α → β → M<VAR>h : ∀ b ∈ s, (Function.mulSupport fun a => f a b).Finite<GOAL>∏ᶠ (a : α), ∏ b ∈ s, f a b = ∏ b ∈ s, ∏ᶠ (a : α), f a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>CommMonoid M<VAR>s : Finset α<VAR>f : α → β → M<VAR>h : ∀ a ∈ s, (Function.mulSupport (f a)).Finite<GOAL>∏ a ∈ s, ∏ᶠ (b : β), f a b = ∏ᶠ (b : β), ∏ a ∈ s, f a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>s : Finset α<VAR>f : α → β → M<VAR>h : ∀ a ∈ s, (Function.support (f a)).Finite<GOAL>∑ a ∈ s, ∑ᶠ (b : β), f a b = ∑ᶠ (b : β), ∑ a ∈ s, f a b
<VAR>α : Type u_1<VAR>R : Type u_7<VAR>Semiring R<VAR>f : α → R<VAR>r : R<VAR>h : (Function.support f).Finite<GOAL>r * ∑ᶠ (a : α), f a = ∑ᶠ (a : α), r * f a
<VAR>α : Type u_1<VAR>R : Type u_7<VAR>Semiring R<VAR>f : α → R<VAR>r : R<VAR>h : (Function.support f).Finite<GOAL>(∑ᶠ (a : α), f a) * r = ∑ᶠ (a : α), f a * r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>DecidableEq β<VAR>s : Finset α<VAR>f : α → M<VAR>g : α → β<GOAL>(Function.support fun b => (Finset.filter (fun a => g a = b) s).sum f) ⊆ ↑(Finset.image g s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>CommMonoid M<VAR>DecidableEq β<VAR>s : Finset α<VAR>f : α → M<VAR>g : α → β<GOAL>(Function.mulSupport fun b => (Finset.filter (fun a => g a = b) s).prod f) ⊆ ↑(Finset.image g s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>CommMonoid M<VAR>DecidableEq α<VAR>DecidableEq β<VAR>s : Finset (α × β)<VAR>f : α × β → M<GOAL>∏ᶠ (ab : α × β) (_ : ab ∈ s), f ab = ∏ᶠ (a : α) (b : β) (_ : b ∈ Finset.image Prod.snd (Finset.filter (fun ab => ab.1 = a) s)), f (a, b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>DecidableEq α<VAR>DecidableEq β<VAR>s : Finset (α × β)<VAR>f : α × β → M<GOAL>∑ᶠ (ab : α × β) (_ : ab ∈ s), f ab = ∑ᶠ (a : α) (b : β) (_ : b ∈ Finset.image Prod.snd (Finset.filter (fun ab => ab.1 = a) s)), f (a, b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>s : Finset (α × β)<VAR>f : α × β → M<GOAL>∑ᶠ (ab : α × β) (_ : ab ∈ s), f ab = ∑ᶠ (a : α) (b : β) (_ : (a, b) ∈ s), f (a, b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>CommMonoid M<VAR>s : Finset (α × β)<VAR>f : α × β → M<GOAL>∏ᶠ (ab : α × β) (_ : ab ∈ s), f ab = ∏ᶠ (a : α) (b : β) (_ : (a, b) ∈ s), f (a, b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>γ : Type u_7<VAR>s : Finset (α × β × γ)<VAR>f : α × β × γ → M<GOAL>∑ᶠ (abc : α × β × γ) (_ : abc ∈ s), f abc = ∑ᶠ (a : α) (b : β) (c : γ) (_ : (a, b, c) ∈ s), f (a, b, c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>CommMonoid M<VAR>γ : Type u_7<VAR>s : Finset (α × β × γ)<VAR>f : α × β × γ → M<GOAL>∏ᶠ (abc : α × β × γ) (_ : abc ∈ s), f abc = ∏ᶠ (a : α) (b : β) (c : γ) (_ : (a, b, c) ∈ s), f (a, b, c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α × β → M<VAR>hf : (Function.support f).Finite<GOAL>∑ᶠ (ab : α × β), f ab = ∑ᶠ (a : α) (b : β), f (a, b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α × β → M<VAR>hf : (Function.mulSupport f).Finite<GOAL>∏ᶠ (ab : α × β), f ab = ∏ᶠ (a : α) (b : β), f (a, b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>CommMonoid M<VAR>γ : Type u_7<VAR>f : α × β × γ → M<VAR>h : (Function.mulSupport f).Finite<GOAL>∏ᶠ (abc : α × β × γ), f abc = ∏ᶠ (a : α) (b : β) (c : γ), f (a, b, c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>γ : Type u_7<VAR>f : α × β × γ → M<VAR>h : (Function.support f).Finite<GOAL>∑ᶠ (abc : α × β × γ), f abc = ∑ᶠ (a : α) (b : β) (c : γ), f (a, b, c)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>s : Set α<VAR>DecidablePred fun x => x ∈ s<VAR>f : (a : α) → a ∈ s → M<GOAL>∏ᶠ (a : α) (h : a ∈ s), f a h = ∏ᶠ (a : α) (_ : a ∈ s), if h' : a ∈ s then f a h' else 1
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>s : Set α<VAR>DecidablePred fun x => x ∈ s<VAR>f : (a : α) → a ∈ s → M<GOAL>∑ᶠ (a : α) (h : a ∈ s), f a h = ∑ᶠ (a : α) (_ : a ∈ s), if h' : a ∈ s then f a h' else 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>DecidablePred fun x => x ∈ Set.range f<VAR>g : α → M<GOAL>(∏ᶠ (b : β), if h : b ∈ Set.range f then g (Classical.choose h) else 1) = ∏ᶠ (a : α), g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>DecidablePred fun x => x ∈ Set.range f<VAR>g : α → M<GOAL>(∑ᶠ (b : β), if h : b ∈ Set.range f then g (Classical.choose h) else 0) = ∑ᶠ (a : α), g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α ↪ β<VAR>DecidablePred fun x => x ∈ Set.range ⇑f<VAR>g : α → M<GOAL>(∏ᶠ (b : β), if h : b ∈ Set.range ⇑f then g (Classical.choose h) else 1) = ∏ᶠ (a : α), g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α ↪ β<VAR>DecidablePred fun x => x ∈ Set.range ⇑f<VAR>g : α → M<GOAL>(∑ᶠ (b : β), if h : b ∈ Set.range ⇑f then g (Classical.choose h) else 0) = ∑ᶠ (a : α), g a
<VAR>α : Type u_1<VAR>CommMonoidWithZero α<VAR>p : α<VAR>hp : Prime p<GOAL>p ≠ 0
<VAR>α : Type u_1<VAR>CommMonoidWithZero α<VAR>p : α<VAR>hp : Prime p<GOAL>¬IsUnit p
<VAR>α : Type u_1<VAR>CommMonoidWithZero α<VAR>p : α<VAR>hp : Prime p<GOAL>¬p ∣ 1
<VAR>α : Type u_1<VAR>CommMonoidWithZero α<VAR>p : α<VAR>hp : Prime p<GOAL>p ≠ 1
<VAR>α : Type u_1<VAR>CommMonoidWithZero α<VAR>p : α<VAR>hp : Prime p<VAR>a b : α<VAR>h : p ∣ a * b<GOAL>p ∣ a ∨ p ∣ b
<VAR>α : Type u_1<VAR>CommMonoidWithZero α<VAR>p : α<VAR>hp : Prime p<VAR>a b : α<GOAL>p ∣ a * b ↔ p ∣ a ∨ p ∣ b
<VAR>α : Type u_1<VAR>CommMonoidWithZero α<VAR>p : α<VAR>hp : Prime p<GOAL>IsPrimal p
<VAR>α : Type u_1<VAR>CommMonoidWithZero α<VAR>p : α<VAR>hp : Prime p<VAR>a b : α<VAR>ha : ¬p ∣ a<VAR>hb : ¬p ∣ b<GOAL>¬p ∣ a * b
<VAR>α : Type u_1<VAR>CommMonoidWithZero α<VAR>p : α<VAR>hp : Prime p<VAR>a : α<VAR>n : ℕ<VAR>h : p ∣ a ^ n<GOAL>p ∣ a
<VAR>α : Type u_1<VAR>CommMonoidWithZero α<VAR>p : α<VAR>hp : Prime p<VAR>a : α<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>p ∣ a ^ n ↔ p ∣ a
<VAR>α : Type u_1<VAR>CommMonoidWithZero α<GOAL>¬Prime 0
<VAR>α : Type u_1<VAR>CommMonoidWithZero α<GOAL>¬Prime 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoidWithZero α<VAR>CommMonoidWithZero β<VAR>F : Type u_5<VAR>G : Type u_6<VAR>FunLike F α β<VAR>MonoidWithZeroHomClass F α β<VAR>FunLike G β α<VAR>MulHomClass G β α<VAR>f : F<VAR>g : G<VAR>p : α<VAR>hinv : ∀ (a : α), g (f a) = a<VAR>hp : Prime (f p)<GOAL>Prime p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoidWithZero α<VAR>CommMonoidWithZero β<VAR>p : α<VAR>e : α ≃* β<GOAL>Prime p ↔ Prime (e p)
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>p : α<VAR>hp : Prime p<VAR>a b : α<GOAL>a ∣ p * b → p ∣ a ∨ a ∣ b
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>p a b : α<VAR>hp : Prime p<VAR>n : ℕ<VAR>h : ¬p ∣ a<VAR>h' : p ^ n ∣ a * b<GOAL>p ^ n ∣ b
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>p a b : α<VAR>hp : Prime p<VAR>n : ℕ<VAR>h : ¬p ∣ b<VAR>h' : p ^ n ∣ a * b<GOAL>p ^ n ∣ a
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>p a b : α<VAR>n : ℕ<VAR>hp : Prime p<VAR>hpow : p ^ n.succ ∣ a ^ n.succ * b ^ n<VAR>hb : ¬p ^ 2 ∣ b<GOAL>p ∣ a
<VAR>α : Type u_5<VAR>CancelCommMonoidWithZero α<VAR>p x y : α<VAR>h : Prime p<VAR>i : ℕ<VAR>hxy : p ^ (i + 1) ∣ x * y<GOAL>p ^ (i + 1) ∣ x ∨ p ∣ y
<VAR>α : Type u_1<VAR>Monoid α<VAR>p : α<VAR>self : Irreducible p<VAR>a b : α<GOAL>p = a * b → IsUnit a ∨ IsUnit b
<VAR>α : Type u_1<VAR>Monoid α<VAR>p : α<VAR>self : Irreducible p<GOAL>¬IsUnit p
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>p : α<VAR>hp : Irreducible p<GOAL>¬p ∣ 1
<VAR>α : Type u_1<VAR>Monoid α<VAR>p : α<VAR>hp : Irreducible p<VAR>a b : α<VAR>h : p = a * b<GOAL>IsUnit a ∨ IsUnit b
<VAR>α : Type u_1<VAR>Monoid α<VAR>p : α<GOAL>Irreducible p ↔ ¬IsUnit p ∧ ∀ (a b : α), p = a * b → IsUnit a ∨ IsUnit b
<VAR>α : Type u_1<VAR>Monoid α<GOAL>¬Irreducible 1
<VAR>α : Type u_1<VAR>Monoid α<VAR>p : α<GOAL>Irreducible p → p ≠ 1
<VAR>α : Type u_1<VAR>MonoidWithZero α<GOAL>¬Irreducible 0
<VAR>α : Type u_1<VAR>MonoidWithZero α<VAR>p : α<GOAL>Irreducible p → p ≠ 0
<VAR>α : Type u_5<VAR>Monoid α<VAR>x y : α<GOAL>Irreducible (x * y) → IsUnit x ∨ IsUnit y
<VAR>α : Type u_5<VAR>Monoid α<VAR>x : α<VAR>n : ℕ<VAR>hn : n ≠ 1<GOAL>¬Irreducible (x ^ n)
<VAR>α : Type u_5<VAR>Monoid α<VAR>x : α<VAR>h : ¬IsUnit x<GOAL>Irreducible x ∨ ∃ a b, ¬IsUnit a ∧ ¬IsUnit b ∧ a * b = x
<VAR>α : Type u_1<VAR>Monoid α<VAR>p q : α<VAR>hp : Irreducible p<VAR>hq : Irreducible q<GOAL>p ∣ q → q ∣ p
<VAR>α : Type u_1<VAR>Monoid α<VAR>p q : α<VAR>hp : Irreducible p<VAR>hq : Irreducible q<GOAL>p ∣ q ↔ q ∣ p
<VAR>α : Type u_1<VAR>Monoid α<VAR>a : αˣ<VAR>b : α<GOAL>Irreducible (↑a * b) ↔ Irreducible b
<VAR>α : Type u_1<VAR>Monoid α<VAR>a b : α<VAR>h : IsUnit a<GOAL>Irreducible (a * b) ↔ Irreducible b
<VAR>α : Type u_1<VAR>Monoid α<VAR>a : αˣ<VAR>b : α<GOAL>Irreducible (b * ↑a) ↔ Irreducible b
<VAR>α : Type u_1<VAR>Monoid α<VAR>a b : α<VAR>h : IsUnit a<GOAL>Irreducible (b * a) ↔ Irreducible b
<VAR>α : Type u_1<VAR>Monoid α<VAR>a b : α<GOAL>Irreducible (a * b) ↔ Irreducible a ∧ IsUnit b ∨ Irreducible b ∧ IsUnit a
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>a : α<VAR>ha : Irreducible a<GOAL>¬IsSquare a
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>a : α<VAR>ha : IsSquare a<GOAL>¬Irreducible a
<VAR>α : Type u_1<VAR>CommMonoidWithZero α<VAR>a : α<VAR>irr : Irreducible a<VAR>primal : IsPrimal a<GOAL>Prime a
<VAR>α : Type u_1<VAR>CommMonoidWithZero α<VAR>DecompositionMonoid α<VAR>a : α<VAR>irr : Irreducible a<GOAL>Prime a
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>p : α<VAR>hp : Prime p<GOAL>Irreducible p
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>DecompositionMonoid α<VAR>a : α<GOAL>Irreducible a ↔ Prime a
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>p : α<VAR>hp : Prime p<VAR>a b : α<VAR>k l : ℕ<GOAL>p ^ k ∣ a → p ^ l ∣ b → p ^ (k + l + 1) ∣ a * b → p ^ (k + 1) ∣ a ∨ p ^ (l + 1) ∣ b
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>p : α<VAR>hp : Prime p<GOAL>¬IsSquare p
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>a : α<VAR>ha : IsSquare a<GOAL>¬Prime a
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>a : α<VAR>n : ℕ<VAR>hn : n ≠ 1<GOAL>¬Prime (a ^ n)
<VAR>α : Type u_1<VAR>Monoid α<VAR>x : α<GOAL>x ~ᵤ x
<VAR>α : Type u_1<VAR>Monoid α<VAR>x y : α<GOAL>x ~ᵤ y → y ~ᵤ x
<VAR>α : Type u_1<VAR>Monoid α<VAR>x y : α<GOAL>x ~ᵤ y ↔ y ~ᵤ x
<VAR>α : Type u_1<VAR>Monoid α<VAR>x y z : α<GOAL>x ~ᵤ y → y ~ᵤ z → x ~ᵤ z
<VAR>M : Type u_5<VAR>N : Type u_6<VAR>Monoid M<VAR>Monoid N<VAR>F : Type u_7<VAR>FunLike F M N<VAR>MonoidHomClass F M N<VAR>f : F<VAR>x y : M<VAR>ha : x ~ᵤ y<GOAL>f x ~ᵤ f y
<VAR>α : Type u_1<VAR>Monoid α<VAR>u : αˣ<GOAL>↑u ~ᵤ 1
<VAR>α : Type u_1<VAR>Monoid α<VAR>a : α<GOAL>a ~ᵤ 1 ↔ IsUnit a
<VAR>α : Type u_1<VAR>MonoidWithZero α<VAR>a : α<GOAL>a ~ᵤ 0 ↔ a = 0
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>a : α<VAR>b : α<VAR>hab : a * b = 1<GOAL>a ~ᵤ 1
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>a b : α<GOAL>a * b ~ᵤ 1 → a ~ᵤ 1
<VAR>β : Type u_5<VAR>Monoid β<VAR>a u : β<VAR>hu : IsUnit u<GOAL>a * u ~ᵤ a
<VAR>β : Type u_5<VAR>CommMonoid β<VAR>a u : β<VAR>hu : IsUnit u<GOAL>u * a ~ᵤ a
<VAR>β : Type u_5<VAR>Monoid β<VAR>a u : β<VAR>hu : IsUnit u<GOAL>a ~ᵤ a * u
<VAR>β : Type u_5<VAR>CommMonoid β<VAR>a u : β<VAR>hu : IsUnit u<GOAL>a ~ᵤ u * a
<VAR>β : Type u_5<VAR>Monoid β<VAR>a u b : β<VAR>hu : IsUnit u<GOAL>a * u ~ᵤ b ↔ a ~ᵤ b
<VAR>β : Type u_5<VAR>CommMonoid β<VAR>u a b : β<VAR>hu : IsUnit u<GOAL>u * a ~ᵤ b ↔ a ~ᵤ b
<VAR>β : Type u_5<VAR>Monoid β<VAR>a b u : β<VAR>hu : IsUnit u<GOAL>a ~ᵤ b * u ↔ a ~ᵤ b
<VAR>β : Type u_5<VAR>CommMonoid β<VAR>a u b : β<VAR>hu : IsUnit u<GOAL>a ~ᵤ u * b ↔ a ~ᵤ b
<VAR>β : Type u_5<VAR>Monoid β<VAR>a b : β<VAR>u : βˣ<GOAL>a * ↑u ~ᵤ b ↔ a ~ᵤ b
<VAR>β : Type u_5<VAR>CommMonoid β<VAR>a b : β<VAR>u : βˣ<GOAL>↑u * a ~ᵤ b ↔ a ~ᵤ b
<VAR>β : Type u_5<VAR>Monoid β<VAR>a b : β<VAR>u : βˣ<GOAL>a ~ᵤ b * ↑u ↔ a ~ᵤ b
<VAR>β : Type u_5<VAR>CommMonoid β<VAR>a b : β<VAR>u : βˣ<GOAL>a ~ᵤ ↑u * b ↔ a ~ᵤ b
<VAR>α : Type u_1<VAR>Monoid α<VAR>a : α<VAR>b c : α<VAR>h : b ~ᵤ c<GOAL>a * b ~ᵤ a * c
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>a b : α<VAR>h : a ~ᵤ b<VAR>c : α<GOAL>a * c ~ᵤ b * c
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>a₁ a₂ b₁ b₂ : α<VAR>h₁ : a₁ ~ᵤ b₁<VAR>h₂ : a₂ ~ᵤ b₂<GOAL>a₁ * a₂ ~ᵤ b₁ * b₂
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>a b : α<VAR>n : ℕ<VAR>h : a ~ᵤ b<GOAL>a ^ n ~ᵤ b ^ n
<VAR>α : Type u_1<VAR>Monoid α<VAR>a b : α<GOAL>a ~ᵤ b → a ∣ b
<VAR>α : Type u_1<VAR>Monoid α<VAR>a b : α<VAR>h : a ~ᵤ b<GOAL>b ∣ a
<VAR>α : Type u_1<VAR>Monoid α<VAR>a b : α<VAR>h : a ~ᵤ b<GOAL>a ∣ b ∧ b ∣ a
<VAR>α : Type u_1<VAR>CancelMonoidWithZero α<VAR>a b : α<VAR>hab : a ∣ b<VAR>hba : b ∣ a<GOAL>a ~ᵤ b
<VAR>α : Type u_1<VAR>CancelMonoidWithZero α<VAR>a b : α<GOAL>a ∣ b ∧ b ∣ a ↔ a ~ᵤ b
<VAR>α : Type u_1<VAR>Monoid α<VAR>a b c : α<VAR>h : a ~ᵤ b<GOAL>a ∣ c ↔ b ∣ c
<VAR>α : Type u_1<VAR>Monoid α<VAR>a b c : α<VAR>h : b ~ᵤ c<GOAL>a ∣ b ↔ a ∣ c
<VAR>α : Type u_1<VAR>MonoidWithZero α<VAR>a b : α<VAR>h : a ~ᵤ b<GOAL>a = 0 ↔ b = 0
<VAR>α : Type u_1<VAR>MonoidWithZero α<VAR>a b : α<VAR>h : a ~ᵤ b<GOAL>a ≠ 0 ↔ b ≠ 0
<VAR>α : Type u_1<VAR>Monoid α<VAR>HasDistribNeg α<VAR>a b : α<VAR>h : a ~ᵤ b<GOAL>-a ~ᵤ b
<VAR>α : Type u_1<VAR>Monoid α<VAR>HasDistribNeg α<VAR>a b : α<VAR>h : a ~ᵤ b<GOAL>a ~ᵤ -b
<VAR>α : Type u_1<VAR>Monoid α<VAR>HasDistribNeg α<VAR>a b : α<VAR>h : a ~ᵤ b<GOAL>-a ~ᵤ -b
<VAR>α : Type u_1<VAR>CommMonoidWithZero α<VAR>p q : α<VAR>h : p ~ᵤ q<VAR>hp : Prime p<GOAL>Prime q
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>x y : α<GOAL>Prime (x * y) ↔ Prime x ∧ IsUnit y ∨ IsUnit x ∧ Prime y
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>p : α<VAR>n : ℕ<GOAL>Prime (p ^ n) ↔ Prime p ∧ n = 1
<VAR>α : Type u_1<VAR>Monoid α<VAR>x y : α<VAR>hx : Irreducible x<GOAL>y ∣ x ↔ IsUnit y ∨ x ~ᵤ y
<VAR>α : Type u_1<VAR>Monoid α<VAR>p q : α<VAR>p_irr : Irreducible p<VAR>q_irr : Irreducible q<VAR>dvd : p ∣ q<GOAL>p ~ᵤ q
<VAR>α : Type u_1<VAR>Monoid α<VAR>p q : α<VAR>pp : Irreducible p<VAR>qp : Irreducible q<GOAL>p ∣ q ↔ p ~ᵤ q
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>p q : α<VAR>p_prime : Prime p<VAR>q_prime : Prime q<VAR>dvd : p ∣ q<GOAL>p ~ᵤ q
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>p q : α<VAR>pp : Prime p<VAR>qp : Prime q<GOAL>p ∣ q ↔ p ~ᵤ q
<VAR>α : Type u_1<VAR>CommMonoidWithZero α<VAR>p q : α<VAR>h : p ~ᵤ q<GOAL>Prime p ↔ Prime q
<VAR>α : Type u_1<VAR>Monoid α<VAR>a b : α<VAR>h : a ~ᵤ b<GOAL>IsUnit a → IsUnit b
<VAR>α : Type u_1<VAR>Monoid α<VAR>a b : α<VAR>h : a ~ᵤ b<GOAL>IsUnit a ↔ IsUnit b
<VAR>α : Type u_1<VAR>Monoid α<VAR>x y : α<VAR>hx : Irreducible x<VAR>hy : y ∣ x<GOAL>IsUnit y ↔ ¬x ~ᵤ y
<VAR>α : Type u_1<VAR>Monoid α<VAR>p q : α<VAR>h : p ~ᵤ q<VAR>hp : Irreducible p<GOAL>Irreducible q
<VAR>α : Type u_1<VAR>Monoid α<VAR>p q : α<VAR>h : p ~ᵤ q<GOAL>Irreducible p ↔ Irreducible q
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>a b c d : α<VAR>h : a * b ~ᵤ c * d<VAR>h₁ : a ~ᵤ c<VAR>ha : a ≠ 0<GOAL>b ~ᵤ d
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>a b c d : α<GOAL>a * b ~ᵤ c * d → b ~ᵤ d → b ≠ 0 → a ~ᵤ c
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>p₁ p₂ : α<VAR>k₁ k₂ : ℕ<VAR>hp₁ : Prime p₁<VAR>hp₂ : Prime p₂<VAR>hk₁ : 0 < k₁<VAR>h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂<GOAL>p₁ ~ᵤ p₂
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>p₁ p₂ : α<VAR>k₁ k₂ : ℕ<VAR>hp₁ : Prime p₁<VAR>hp₂ : Prime p₂<VAR>hk₂ : 0 < k₂<VAR>h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂<GOAL>p₁ ~ᵤ p₂
<VAR>α : Type u_1<VAR>Monoid α<VAR>p n : α<VAR>hp : Irreducible p<GOAL>IsRelPrime p n ↔ ¬p ∣ n
<VAR>α : Type u_1<VAR>Monoid α<VAR>p n : α<VAR>hp : Irreducible p<GOAL>p ∣ n ∨ IsRelPrime p n
<VAR>α : Type u_1<VAR>Monoid α<VAR>Unique αˣ<VAR>x y : α<GOAL>x ~ᵤ y ↔ x = y
<VAR>α : Type u_1<VAR>Monoid α<VAR>Unique αˣ<GOAL>Associated = Eq
<VAR>M : Type u_5<VAR>CancelCommMonoidWithZero M<VAR>Unique Mˣ<VAR>p q : M<VAR>pp : Prime p<VAR>qp : Prime q<GOAL>p ∣ q ↔ p = q
<VAR>R : Type u_5<VAR>CancelCommMonoidWithZero R<VAR>Unique Rˣ<VAR>p₁ p₂ : R<VAR>k₁ k₂ : ℕ<VAR>hp₁ : Prime p₁<VAR>hp₂ : Prime p₂<VAR>hk₁ : 0 < k₁<VAR>h : p₁ ^ k₁ = p₂ ^ k₂<GOAL>p₁ = p₂
<VAR>R : Type u_5<VAR>CancelCommMonoidWithZero R<VAR>Unique Rˣ<VAR>p₁ p₂ : R<VAR>k₁ k₂ : ℕ<VAR>hp₁ : Prime p₁<VAR>hp₂ : Prime p₂<VAR>hk₁ : 0 < k₂<VAR>h : p₁ ^ k₁ = p₂ ^ k₂<GOAL>p₁ = p₂
<VAR>α : Type u_1<VAR>Monoid α<VAR>a b : α<GOAL>Associates.mk a = Associates.mk b ↔ a ~ᵤ b
<VAR>α : Type u_1<VAR>Monoid α<VAR>a : α<GOAL>⟦a⟧ = Associates.mk a
<VAR>α : Type u_1<VAR>Monoid α<VAR>a : α<GOAL>Quot.mk Setoid.r a = Associates.mk a
<VAR>α : Type u_1<VAR>Monoid α<VAR>a : Associates α<GOAL>Associates.mk (Quot.out a) = a
<VAR>α : Type u_1<VAR>Monoid α<VAR>a : α<GOAL>Quot.out (Associates.mk a) ~ᵤ a
<VAR>α : Type u_1<VAR>Monoid α<VAR>p : Associates α → Prop<GOAL>(∀ (a : Associates α), p a) ↔ ∀ (a : α), p (Associates.mk a)
<VAR>α : Type u_1<VAR>Monoid α<GOAL>Function.Surjective Associates.mk
<VAR>α : Type u_1<VAR>Monoid α<GOAL>Associates.mk 1 = 1
<VAR>α : Type u_1<VAR>Monoid α<GOAL>1 = Associates.mk 1
<VAR>α : Type u_1<VAR>Monoid α<VAR>a : α<GOAL>Associates.mk a = 1 ↔ IsUnit a
<VAR>α : Type u_1<VAR>Monoid α<GOAL>⊥ = 1
<VAR>α : Type u_1<VAR>Monoid α<VAR>a : Associates α<GOAL>∃ a0, Associates.mk a0 = a