ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>Group G<VAR>s t : Set G<VAR>ht : IsSubgroup t<VAR>h : s ⊆ t<GOAL>Group.closure s ⊆ t
<VAR>G : Type u_1<VAR>Group G<VAR>s t : Set G<VAR>ht : IsSubgroup t<GOAL>Group.closure s ⊆ t ↔ s ⊆ t
<VAR>G : Type u_1<VAR>AddGroup G<VAR>s t : Set G<VAR>ht : IsAddSubgroup t<GOAL>AddGroup.closure s ⊆ t ↔ s ⊆ t
<VAR>G : Type u_1<VAR>Group G<VAR>s t : Set G<VAR>h : s ⊆ t<GOAL>Group.closure s ⊆ Group.closure t
<VAR>G : Type u_1<VAR>AddGroup G<VAR>s t : Set G<VAR>h : s ⊆ t<GOAL>AddGroup.closure s ⊆ AddGroup.closure t
<VAR>G : Type u_1<VAR>Group G<VAR>s : Set G<VAR>hs : IsSubgroup s<GOAL>Group.closure s = s
<VAR>G : Type u_1<VAR>AddGroup G<VAR>s : Set G<VAR>hs : IsAddSubgroup s<GOAL>AddGroup.closure s = s
<VAR>G : Type u_1<VAR>AddGroup G<VAR>s : Set G<VAR>a : G<VAR>h : a ∈ AddGroup.closure s<GOAL>∃ l, (∀ x ∈ l, x ∈ s ∨ -x ∈ s) ∧ l.sum = a
<VAR>G : Type u_1<VAR>Group G<VAR>s : Set G<VAR>a : G<VAR>h : a ∈ Group.closure s<GOAL>∃ l, (∀ x ∈ l, x ∈ s ∨ x⁻¹ ∈ s) ∧ l.prod = a
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>AddGroup G<VAR>AddGroup H<VAR>f : G → H<VAR>hf : IsAddGroupHom f<VAR>s : Set G<GOAL>f '' AddGroup.closure s = AddGroup.closure (f '' s)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Group G<VAR>Group H<VAR>f : G → H<VAR>hf : IsGroupHom f<VAR>s : Set G<GOAL>f '' Group.closure s = Group.closure (f '' s)
<VAR>G : Type u_1<VAR>Group G<VAR>s : Set G<GOAL>Monoid.Closure s ⊆ Group.closure s
<VAR>G : Type u_1<VAR>AddGroup G<VAR>s : Set G<GOAL>AddMonoid.Closure s ⊆ AddGroup.closure s
<VAR>G : Type u_1<VAR>Group G<VAR>s : Set G<GOAL>Monoid.Closure (Inv.inv ⁻¹' s) ⊆ Group.closure s
<VAR>G : Type u_1<VAR>AddGroup G<VAR>s : Set G<GOAL>AddMonoid.Closure (Neg.neg ⁻¹' s) ⊆ AddGroup.closure s
<VAR>G : Type u_1<VAR>Group G<VAR>s : Set G<GOAL>Group.closure s = Monoid.Closure (s ∪ Inv.inv ⁻¹' s)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>s : Set G<GOAL>AddGroup.closure s = AddMonoid.Closure (s ∪ Neg.neg ⁻¹' s)
<VAR>G : Type u_4<VAR>AddCommGroup G<VAR>s t : Set G<VAR>x : G<GOAL>x ∈ AddGroup.closure (s ∪ t) ↔ ∃ y ∈ AddGroup.closure s, ∃ z ∈ AddGroup.closure t, y + z = x
<VAR>G : Type u_4<VAR>CommGroup G<VAR>s t : Set G<VAR>x : G<GOAL>x ∈ Group.closure (s ∪ t) ↔ ∃ y ∈ Group.closure s, ∃ z ∈ Group.closure t, y * z = x
<VAR>G : Type u_1<VAR>Group G<GOAL>IsSubgroup.trivial G = Group.closure ∅
<VAR>G : Type u_1<VAR>AddGroup G<GOAL>IsAddSubgroup.trivial G = AddGroup.closure ∅
<VAR>G : Type u_1<VAR>Group G<VAR>t : Set G<VAR>ht : IsNormalSubgroup t<VAR>a : G<VAR>h : a ∈ t<GOAL>conjugatesOf a ⊆ t
<VAR>G : Type u_1<VAR>Group G<VAR>s t : Set G<VAR>ht : IsNormalSubgroup t<VAR>h : s ⊆ t<GOAL>Group.conjugatesOfSet s ⊆ t
<VAR>G : Type u_1<VAR>s : Set G<VAR>Group G<GOAL>Group.conjugatesOfSet s ⊆ Group.normalClosure s
<VAR>G : Type u_1<VAR>s : Set G<VAR>Group G<GOAL>s ⊆ Group.normalClosure s
<VAR>G : Type u_1<VAR>Group G<VAR>s : Set G<GOAL>IsSubgroup (Group.normalClosure s)
<VAR>G : Type u_1<VAR>s : Set G<VAR>Group G<GOAL>IsNormalSubgroup (Group.normalClosure s)
<VAR>G : Type u_1<VAR>Group G<VAR>s t : Set G<VAR>ht : IsNormalSubgroup t<VAR>h : s ⊆ t<GOAL>Group.normalClosure s ⊆ t
<VAR>G : Type u_1<VAR>Group G<VAR>s t : Set G<VAR>ht : IsNormalSubgroup t<GOAL>s ⊆ t ↔ Group.normalClosure s ⊆ t
<VAR>G : Type u_1<VAR>Group G<VAR>s t : Set G<GOAL>s ⊆ t → Group.normalClosure s ⊆ Group.normalClosure t
<VAR>G : Type u_1<VAR>AddGroup G<VAR>K : AddSubgroup G<GOAL>IsAddSubgroup ↑K
<VAR>G : Type u_1<VAR>Group G<VAR>K : Subgroup G<GOAL>IsSubgroup ↑K
<VAR>G : Type u_1<VAR>Group G<VAR>s : Set G<VAR>h : IsSubgroup s<VAR>n : IsNormalSubgroup s<GOAL>(Subgroup.of h).Normal
<VAR>G : Type u_1<VAR>AddGroup G<VAR>s : Set G<VAR>h : IsAddSubgroup s<VAR>n : IsNormalAddSubgroup s<GOAL>(AddSubgroup.of h).Normal
<VAR>X : AlgebraicGeometry.Scheme<VAR>x : ↑↑∅.toPresheafedSpace<GOAL>X.emptyTo.val.base x = PEmpty.elim x
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : (TopologicalSpace.Opens ↑↑X.toPresheafedSpace)ᵒᵖ<GOAL>X.emptyTo.val.c.app U = CommRingCat.punitIsTerminal.from (X.presheaf.obj U)
<VAR>X : AlgebraicGeometry.Scheme<VAR>f g : ∅ ⟶ X<GOAL>f = g
<VAR>X : AlgebraicGeometry.Scheme<VAR>f : ∅ ⟶ X<GOAL>f = X.emptyTo
<GOAL>AlgebraicGeometry.emptyIsInitial.to = AlgebraicGeometry.Scheme.emptyTo
<VAR>X : AlgebraicGeometry.Scheme<GOAL>AlgebraicGeometry.IsAffineOpen ⊥
<VAR>ι : Type u<VAR>f : ι → AlgebraicGeometry.Scheme<GOAL>∀ (x x_1 : ι) (x_2 : x ≠ x_1), (AlgebraicGeometry.disjointGlueData' f).t x x_1 x_2 = 𝟙 ((fun x x_3 x => ∅) x x_1 x_2)
<VAR>ι : Type u<VAR>f : ι → AlgebraicGeometry.Scheme<GOAL>(AlgebraicGeometry.disjointGlueData' f).J = ι
<VAR>ι : Type u<VAR>f : ι → AlgebraicGeometry.Scheme<GOAL>∀ (a : ι), (AlgebraicGeometry.disjointGlueData' f).U a = f a
<VAR>ι : Type u<VAR>f : ι → AlgebraicGeometry.Scheme<GOAL>∀ (x x_1 : ι) (x_2 : x ≠ x_1), (AlgebraicGeometry.disjointGlueData' f).f x x_1 x_2 = (f x).emptyTo
<VAR>ι : Type u<VAR>f : ι → AlgebraicGeometry.Scheme<GOAL>∀ (x x_1 x_2 : ι) (x_3 : x ≠ x_1) (x_4 : x ≠ x_2) (x_5 : x_1 ≠ x_2), (AlgebraicGeometry.disjointGlueData' f).t' x x_1 x_2 x_3 x_4 x_5 = CategoryTheory.Limits.pullback.fst ((fun x x_6 x_7 => (f x).emptyTo) x x_1 x_3) ((fun x x_6 x_7 => (f x).emptyTo) x x_2 x_4) ≫ (CategoryTheory.Limits.pullback ((fun x x_6 x_7 => (f x).emptyTo) x_1 x_2 x_5) ((fun x x_6 x_7 => (f x).emptyTo) x_1 x ⋯)).emptyTo
<VAR>ι : Type u<VAR>f : ι → AlgebraicGeometry.Scheme<GOAL>∀ (x x_1 : ι) (x_2 : x ≠ x_1), (AlgebraicGeometry.disjointGlueData' f).V x x_1 x_2 = ∅
<VAR>ι : Type u<VAR>f : ι → AlgebraicGeometry.Scheme<VAR>i j : (AlgebraicGeometry.disjointGlueData' f).J<GOAL>(AlgebraicGeometry.disjointGlueData f).f i j = (AlgebraicGeometry.disjointGlueData' f).f' i j
<VAR>ι : Type u<VAR>f : ι → AlgebraicGeometry.Scheme<VAR>ij : (AlgebraicGeometry.disjointGlueData' f).J × (AlgebraicGeometry.disjointGlueData' f).J<GOAL>(AlgebraicGeometry.disjointGlueData f).V ij = if ij.1 = ij.2 then f ij.1 else ∅
<VAR>ι : Type u<VAR>f : ι → AlgebraicGeometry.Scheme<VAR>i j : (AlgebraicGeometry.disjointGlueData' f).J<GOAL>(AlgebraicGeometry.disjointGlueData f).t i j = if h : i = j then CategoryTheory.eqToHom ⋯ else CategoryTheory.eqToHom ⋯
<VAR>ι : Type u<VAR>f : ι → AlgebraicGeometry.Scheme<GOAL>(AlgebraicGeometry.disjointGlueData f).J = ι
<VAR>ι : Type u<VAR>f : ι → AlgebraicGeometry.Scheme<GOAL>∀ (a : (AlgebraicGeometry.disjointGlueData' f).J), (AlgebraicGeometry.disjointGlueData f).U a = f a
<VAR>ι : Type u<VAR>f : ι → AlgebraicGeometry.Scheme<VAR>i : (AlgebraicGeometry.disjointGlueData f).J<GOAL>(AlgebraicGeometry.disjointGlueData f).ι i ≫ (AlgebraicGeometry.sigmaIsoGlued f).inv = CategoryTheory.Limits.Sigma.ι f i
<VAR>ι : Type u<VAR>f : ι → AlgebraicGeometry.Scheme<VAR>i : ι<GOAL>CategoryTheory.Limits.Sigma.ι f i ≫ (AlgebraicGeometry.sigmaIsoGlued f).hom = (AlgebraicGeometry.disjointGlueData f).ι i
<VAR>ι : Type u<VAR>f : ι → AlgebraicGeometry.Scheme<VAR>i j : ι<VAR>x : ↑↑(f i).toPresheafedSpace<VAR>y : ↑↑(f j).toPresheafedSpace<GOAL>(CategoryTheory.Limits.Sigma.ι f i).val.base x = (CategoryTheory.Limits.Sigma.ι f j).val.base y ↔ ⟨i, x⟩ = ⟨j, y⟩
<VAR>ι : Type u<VAR>f : ι → AlgebraicGeometry.Scheme<VAR>i j : ι<VAR>h : i ≠ j<GOAL>Disjoint (AlgebraicGeometry.Scheme.Hom.opensRange (CategoryTheory.Limits.Sigma.ι f i)) (AlgebraicGeometry.Scheme.Hom.opensRange (CategoryTheory.Limits.Sigma.ι f j))
<VAR>ι : Type u<VAR>f : ι → AlgebraicGeometry.Scheme<VAR>x : ↑↑(∐ f).toPresheafedSpace<GOAL>∃ i y, (CategoryTheory.Limits.Sigma.ι f i).val.base y = x
<VAR>ι : Type u<VAR>f : ι → AlgebraicGeometry.Scheme<GOAL>⨆ i, AlgebraicGeometry.Scheme.Hom.opensRange (CategoryTheory.Limits.Sigma.ι f i) = ⊤
<VAR>ι : Type u<VAR>f : ι → AlgebraicGeometry.Scheme<VAR>b : ι<GOAL>(AlgebraicGeometry.sigmaOpenCover f).map b = CategoryTheory.Limits.Sigma.ι f b
<VAR>ι : Type u<VAR>f : ι → AlgebraicGeometry.Scheme<GOAL>∀ (a : ι), (AlgebraicGeometry.sigmaOpenCover f).obj a = f a
<VAR>ι : Type u<VAR>f : ι → AlgebraicGeometry.Scheme<VAR>i : ι<VAR>x : ↑↑(f i).toPresheafedSpace<GOAL>(AlgebraicGeometry.sigmaMk f) ⟨i, x⟩ = (CategoryTheory.Limits.Sigma.ι f i).val.base x
<VAR>α : Type u_2<VAR>CancelCommMonoidWithZero α<VAR>self : NormalizationMonoid α<VAR>u : αˣ<GOAL>normUnit ↑u = u⁻¹
<VAR>α : Type u_2<VAR>CancelCommMonoidWithZero α<VAR>self : NormalizationMonoid α<GOAL>normUnit 0 = 1
<VAR>α : Type u_2<VAR>CancelCommMonoidWithZero α<VAR>self : NormalizationMonoid α<VAR>a b : α<GOAL>a ≠ 0 → b ≠ 0 → normUnit (a * b) = normUnit a * normUnit b
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<GOAL>normUnit 1 = 1
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<VAR>x : α<GOAL>Associated x (normalize x)
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<VAR>x : α<GOAL>Associated (normalize x) x
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<VAR>x y : α<GOAL>Associated x (normalize y) ↔ Associated x y
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<VAR>x y : α<GOAL>Associated (normalize x) y ↔ Associated x y
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<VAR>x : α<GOAL>Associates.mk (normalize x) = Associates.mk x
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<VAR>x : α<GOAL>normalize x = x * ↑(normUnit x)
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<GOAL>normalize 0 = 0
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<GOAL>normalize 1 = 1
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<VAR>u : αˣ<GOAL>normalize ↑u = 1
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<VAR>x : α<GOAL>normalize x = 0 ↔ x = 0
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<VAR>x : α<GOAL>normalize x = 1 ↔ IsUnit x
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<VAR>a : α<GOAL>normUnit (a * ↑(normUnit a)) = 1
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<VAR>x : α<GOAL>normalize (normalize x) = normalize x
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<VAR>a b : α<VAR>hab : a ∣ b<VAR>hba : b ∣ a<GOAL>normalize a = normalize b
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<VAR>x y : α<GOAL>normalize x = normalize y ↔ x ∣ y ∧ y ∣ x
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<VAR>a b : α<VAR>ha : normalize a = a<VAR>hb : normalize b = b<VAR>hab : a ∣ b<VAR>hba : b ∣ a<GOAL>a = b
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<VAR>a b : α<VAR>h : Associated a b<VAR>ha : normalize a = a<VAR>hb : normalize b = b<GOAL>a = b
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<VAR>a b : α<GOAL>a ∣ normalize b ↔ a ∣ b
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<VAR>a b : α<GOAL>normalize a ∣ b ↔ a ∣ b
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<VAR>a : α<GOAL>(Associates.mk a).out = normalize a
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<GOAL>Associates.out 1 = 1
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<VAR>a b : Associates α<GOAL>(a * b).out = a.out * b.out
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<VAR>a : α<VAR>b : Associates α<GOAL>a ∣ b.out ↔ Associates.mk a ≤ b
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<VAR>a : α<VAR>b : Associates α<GOAL>b.out ∣ a ↔ b ≤ Associates.mk a
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<GOAL>⊤.out = 0
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<VAR>a : Associates α<GOAL>normalize a.out = a.out
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<VAR>a : Associates α<GOAL>Associates.mk a.out = a
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<GOAL>Function.Injective Associates.out
<VAR>α : Type u_2<VAR>CancelCommMonoidWithZero α<VAR>self : GCDMonoid α<VAR>a : α<GOAL>lcm 0 a = 0
<VAR>α : Type u_2<VAR>CancelCommMonoidWithZero α<VAR>self : GCDMonoid α<VAR>a b c : α<GOAL>a ∣ c → a ∣ b → a ∣ gcd c b
<VAR>α : Type u_2<VAR>CancelCommMonoidWithZero α<VAR>self : GCDMonoid α<VAR>a b : α<GOAL>Associated (gcd a b * lcm a b) (a * b)
<VAR>α : Type u_2<VAR>CancelCommMonoidWithZero α<VAR>self : GCDMonoid α<VAR>a : α<GOAL>lcm a 0 = 0
<VAR>α : Type u_2<VAR>CancelCommMonoidWithZero α<VAR>self : GCDMonoid α<VAR>a b : α<GOAL>gcd a b ∣ b
<VAR>α : Type u_2<VAR>CancelCommMonoidWithZero α<VAR>self : GCDMonoid α<VAR>a b : α<GOAL>gcd a b ∣ a
<VAR>α : Type u_2<VAR>CancelCommMonoidWithZero α<VAR>self : NormalizedGCDMonoid α<VAR>a b : α<GOAL>normalize (gcd a b) = gcd a b
<VAR>α : Type u_2<VAR>CancelCommMonoidWithZero α<VAR>self : NormalizedGCDMonoid α<VAR>a b : α<GOAL>normalize (lcm a b) = lcm a b
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>a b : α<GOAL>IsUnit (gcd a b) ↔ IsRelPrime a b
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>a b : α<GOAL>normalize (gcd a b) = gcd a b
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>a b : α<GOAL>Associated (gcd a b * lcm a b) (a * b)
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>a b c : α<GOAL>a ∣ gcd b c ↔ a ∣ b ∧ a ∣ c
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>a b : α<GOAL>gcd a b = gcd b a
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>a b : α<GOAL>Associated (gcd a b) (gcd b a)
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>m n k : α<GOAL>gcd (gcd m n) k = gcd m (gcd n k)
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>m n k : α<GOAL>Associated (gcd (gcd m n) k) (gcd m (gcd n k))
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>a b c : α<VAR>habc : gcd a b ∣ c<VAR>hcab : c ∣ gcd a b<GOAL>gcd a b = normalize c
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>a : α<GOAL>gcd 0 a = normalize a
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>a : α<GOAL>Associated (gcd 0 a) a
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>a : α<GOAL>gcd a 0 = normalize a
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>a : α<GOAL>Associated (gcd a 0) a
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>a b : α<GOAL>gcd a b = 0 ↔ a = 0 ∧ b = 0
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>a : α<GOAL>gcd 1 a = 1
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>a : α<GOAL>IsUnit (gcd 1 a)
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>a : α<GOAL>Associated (gcd 1 a) 1
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>a : α<GOAL>gcd a 1 = 1
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>a : α<GOAL>IsUnit (gcd a 1)
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>a : α<GOAL>Associated (gcd a 1) 1
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>a b c d : α<VAR>hab : a ∣ b<VAR>hcd : c ∣ d<GOAL>gcd a c ∣ gcd b d
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>a₁ a₂ b₁ b₂ : α<VAR>ha : Associated a₁ a₂<VAR>hb : Associated b₁ b₂<GOAL>Associated (gcd a₁ b₁) (gcd a₂ b₂)
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>a : α<GOAL>gcd a a = normalize a
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>a b c : α<GOAL>gcd (a * b) (a * c) = normalize a * gcd b c
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>a b c : α<GOAL>Associated (gcd (a * b) (a * c)) (a * gcd b c)
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>a b c : α<GOAL>gcd (b * a) (c * a) = gcd b c * normalize a
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>a b c : α<GOAL>Associated (gcd (b * a) (c * a)) (gcd b c * a)
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>a b : α<VAR>h : normalize a = a<GOAL>gcd a b = a ↔ a ∣ b
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>a b : α<VAR>h : normalize b = b<GOAL>gcd a b = b ↔ b ∣ a
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>m n k : α<GOAL>gcd m n ∣ gcd (k * m) n
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>m n k : α<GOAL>gcd m n ∣ gcd (m * k) n
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>m n k : α<GOAL>gcd m n ∣ gcd m (k * n)
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>m n k : α<GOAL>gcd m n ∣ gcd m (n * k)
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>m n : α<VAR>h : Associated m n<VAR>k : α<GOAL>gcd m k = gcd n k
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>m n : α<VAR>h : Associated m n<VAR>k : α<GOAL>gcd k m = gcd k n
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>m n k : α<VAR>H : k ∣ m * n<GOAL>k ∣ gcd k m * n
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>m n k : α<GOAL>k ∣ gcd k m * n ↔ k ∣ m * n
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>m n k : α<VAR>H : k ∣ m * n<GOAL>k ∣ m * gcd k n
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>m n k : α<GOAL>k ∣ m * gcd k n ↔ k ∣ m * n
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>k m n : α<GOAL>gcd k (m * n) ∣ gcd k m * gcd k n
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>a b : α<VAR>k : ℕ<GOAL>gcd a (b ^ k) ∣ gcd a b ^ k
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>a b : α<VAR>k : ℕ<GOAL>gcd (a ^ k) b ∣ gcd a b ^ k
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>a b c d₁ d₂ : α<VAR>ha : a ≠ 0<VAR>hab : IsUnit (gcd a b)<VAR>k : ℕ<VAR>h : a * b = c ^ k<VAR>hc : c = d₁ * d₂<VAR>hd₁ : d₁ ∣ a<GOAL>d₁ ^ k ≠ 0 ∧ d₁ ^ k ∣ a
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>a b c : α<VAR>hab : IsUnit (gcd a b)<VAR>k : ℕ<VAR>h : a * b = c ^ k<GOAL>∃ d, Associated (d ^ k) a
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>Unique αˣ<VAR>a b c : α<VAR>hab : IsUnit (gcd a b)<VAR>k : ℕ<VAR>h : a * b = c ^ k<GOAL>∃ d, a = d ^ k
<VAR>α : Type u_2<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>a b d : α<VAR>hda : d ∣ a<VAR>hdb : d ∣ b<VAR>hd : ∀ (e : α), e ∣ a → e ∣ b → e ∣ d<GOAL>gcd a b = normalize d
<VAR>α : Type u_2<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>a b d : α<VAR>hda : d ∣ a<VAR>hdb : d ∣ b<VAR>hd : ∀ (e : α), e ∣ a → e ∣ b → e ∣ d<GOAL>Associated d (gcd a b)
<VAR>α : Type u_2<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>x y x' y' : α<VAR>ex : x = gcd x y * x'<VAR>ey : y = gcd x y * y'<VAR>h : gcd x y ≠ 0<GOAL>IsUnit (gcd x' y')
<VAR>α : Type u_2<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>x y : α<GOAL>∃ x' y', x = gcd x y * x' ∧ y = gcd x y * y' ∧ IsUnit (gcd x' y')
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>x y : α<GOAL>Associated x (gcd x y) ↔ x ∣ y
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>x y : α<GOAL>Associated y (gcd x y) ↔ y ∣ x
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>x y : α<VAR>hx : Irreducible x<GOAL>IsUnit (gcd x y) ↔ ¬x ∣ y
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>x y : α<VAR>hx : Irreducible x<GOAL>gcd x y = 1 ↔ ¬x ∣ y
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>HasDistribNeg α<VAR>GCDMonoid α<VAR>a b : α<GOAL>Associated (gcd a (-b)) (gcd a b)
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>HasDistribNeg α<VAR>NormalizedGCDMonoid α<VAR>a b : α<GOAL>gcd a (-b) = gcd a b
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>HasDistribNeg α<VAR>GCDMonoid α<VAR>a b : α<GOAL>Associated (gcd (-a) b) (gcd a b)
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>HasDistribNeg α<VAR>NormalizedGCDMonoid α<VAR>a b : α<GOAL>gcd (-a) b = gcd a b
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>a b c : α<GOAL>lcm a b ∣ c ↔ a ∣ c ∧ b ∣ c
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>a b : α<GOAL>a ∣ lcm a b
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>a b : α<GOAL>b ∣ lcm a b
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>a b c : α<VAR>hab : a ∣ b<VAR>hcb : c ∣ b<GOAL>lcm a c ∣ b
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>a b : α<GOAL>lcm a b = 0 ↔ a = 0 ∨ b = 0
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>a b : α<GOAL>normalize (lcm a b) = lcm a b
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>a b : α<GOAL>lcm a b = lcm b a
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>a b : α<GOAL>Associated (lcm a b) (lcm b a)
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>m n k : α<GOAL>lcm (lcm m n) k = lcm m (lcm n k)
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>m n k : α<GOAL>Associated (lcm (lcm m n) k) (lcm m (lcm n k))
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>a b c : α<VAR>habc : lcm a b ∣ c<VAR>hcab : c ∣ lcm a b<GOAL>lcm a b = normalize c
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>a b c d : α<VAR>hab : a ∣ b<VAR>hcd : c ∣ d<GOAL>lcm a c ∣ lcm b d
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>a₁ a₂ b₁ b₂ : α<VAR>ha : Associated a₁ a₂<VAR>hb : Associated b₁ b₂<GOAL>Associated (lcm a₁ b₁) (lcm a₂ b₂)
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>u : αˣ<VAR>a : α<GOAL>lcm (↑u) a = normalize a
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>a : α<VAR>u : αˣ<GOAL>lcm a ↑u = normalize a
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>a : α<GOAL>lcm 1 a = normalize a
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>a : α<GOAL>lcm a 1 = normalize a
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>a : α<GOAL>lcm a a = normalize a
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>a b : α<GOAL>lcm a b = 1 ↔ a ∣ 1 ∧ b ∣ 1
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>a b c : α<GOAL>lcm (a * b) (a * c) = normalize a * lcm b c
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>a b c : α<GOAL>lcm (b * a) (c * a) = lcm b c * normalize a
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>a b : α<VAR>h : normalize a = a<GOAL>lcm a b = a ↔ b ∣ a
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>a b : α<VAR>h : normalize b = b<GOAL>lcm a b = b ↔ a ∣ b
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>m n k : α<GOAL>lcm m n ∣ lcm (k * m) n
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>m n k : α<GOAL>lcm m n ∣ lcm (m * k) n
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>m n k : α<GOAL>lcm m n ∣ lcm m (k * n)
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>m n k : α<GOAL>lcm m n ∣ lcm m (n * k)
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>m n : α<VAR>h : Associated m n<VAR>k : α<GOAL>lcm m k = lcm n k
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>m n : α<VAR>h : Associated m n<VAR>k : α<GOAL>lcm k m = lcm k n
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>Unique αˣ<VAR>x : α<GOAL>normUnit x = 1
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>Unique αˣ<VAR>x : α<GOAL>normalize x = x
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>Unique αˣ<GOAL>∀ (a : Associates α), associatesEquivOfUniqueUnits a = a.out
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>Unique αˣ<VAR>a : α<GOAL>associatesEquivOfUniqueUnits.symm a = Associates.mk a
<VAR>α : Type u_1<VAR>CommRing α<VAR>IsDomain α<VAR>NormalizedGCDMonoid α<VAR>a b c : α<VAR>h : a ∣ b - c<GOAL>gcd a b = gcd a c