ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>AddGroup α<VAR>s : AddSubgroup α<VAR>a : α<VAR>ha : a ∈ s<GOAL>a +ᵥ ↑s = ↑s
<VAR>α : Type u_1<VAR>Group α<VAR>s : Subgroup α<VAR>a : α<VAR>ha : a ∈ s<GOAL>a • ↑s = ↑s
<VAR>α : Type u_1<VAR>AddGroup α<VAR>s : AddSubgroup α<VAR>a : α<VAR>ha : a ∈ s<GOAL>AddOpposite.op a +ᵥ ↑s = ↑s
<VAR>α : Type u_1<VAR>Group α<VAR>s : Subgroup α<VAR>a : α<VAR>ha : a ∈ s<GOAL>MulOpposite.op a • ↑s = ↑s
<VAR>α : Type u_1<VAR>AddGroup α<VAR>s : AddSubgroup α<VAR>a : α<GOAL>AddAction.orbit (↥s) a = AddOpposite.op a +ᵥ ↑s
<VAR>α : Type u_1<VAR>Group α<VAR>s : Subgroup α<VAR>a : α<GOAL>MulAction.orbit (↥s) a = MulOpposite.op a • ↑s
<VAR>α : Type u_1<VAR>AddGroup α<VAR>s : AddSubgroup α<VAR>a : α<VAR>ha : a ∈ s<GOAL>AddAction.orbit (↥s) a = ↑s
<VAR>α : Type u_1<VAR>Group α<VAR>s : Subgroup α<VAR>a : α<VAR>ha : a ∈ s<GOAL>MulAction.orbit (↥s) a = ↑s
<VAR>α : Type u_1<VAR>Group α<VAR>s : Subgroup α<GOAL>MulAction.orbit (↥s) 1 = ↑s
<VAR>α : Type u_1<VAR>AddGroup α<VAR>s : AddSubgroup α<GOAL>AddAction.orbit (↥s) 0 = ↑s
<VAR>α : Type u_1<VAR>Group α<VAR>s : Subgroup α<VAR>N : s.Normal<VAR>g : α<GOAL>g • ↑s = MulOpposite.op g • ↑s
<VAR>α : Type u_1<VAR>AddGroup α<VAR>s : AddSubgroup α<VAR>N : s.Normal<VAR>g : α<GOAL>g +ᵥ ↑s = AddOpposite.op g +ᵥ ↑s
<VAR>α : Type u_1<VAR>AddGroup α<VAR>s : AddSubgroup α<VAR>h : ∀ (g : α), g +ᵥ ↑s = AddOpposite.op g +ᵥ ↑s<GOAL>s.Normal
<VAR>α : Type u_1<VAR>Group α<VAR>s : Subgroup α<VAR>h : ∀ (g : α), g • ↑s = MulOpposite.op g • ↑s<GOAL>s.Normal
<VAR>α : Type u_1<VAR>Group α<VAR>s : Subgroup α<GOAL>s.Normal ↔ ∀ (g : α), g • ↑s = MulOpposite.op g • ↑s
<VAR>α : Type u_1<VAR>AddGroup α<VAR>s : AddSubgroup α<GOAL>s.Normal ↔ ∀ (g : α), g +ᵥ ↑s = AddOpposite.op g +ᵥ ↑s
<VAR>α : Type u_1<VAR>Group α<VAR>s : Subgroup α<VAR>x y : α<GOAL>x • ↑s = y • ↑s ↔ x⁻¹ * y ∈ s
<VAR>α : Type u_1<VAR>AddGroup α<VAR>s : AddSubgroup α<VAR>x y : α<GOAL>x +ᵥ ↑s = y +ᵥ ↑s ↔ -x + y ∈ s
<VAR>α : Type u_1<VAR>Group α<VAR>s : Subgroup α<VAR>x y : α<GOAL>MulOpposite.op x • ↑s = MulOpposite.op y • ↑s ↔ y * x⁻¹ ∈ s
<VAR>α : Type u_1<VAR>AddGroup α<VAR>s : AddSubgroup α<VAR>x y : α<GOAL>AddOpposite.op x +ᵥ ↑s = AddOpposite.op y +ᵥ ↑s ↔ y + -x ∈ s
<VAR>α : Type u_1<VAR>AddGroup α<VAR>s : AddSubgroup α<VAR>x y : α<GOAL>Setoid.r x y ↔ -x + y ∈ s
<VAR>α : Type u_1<VAR>Group α<VAR>s : Subgroup α<VAR>x y : α<GOAL>Setoid.r x y ↔ x⁻¹ * y ∈ s
<VAR>α : Type u_1<VAR>Group α<VAR>s : Subgroup α<GOAL>Setoid.r = fun x y => x⁻¹ * y ∈ s
<VAR>α : Type u_1<VAR>AddGroup α<VAR>s : AddSubgroup α<GOAL>Setoid.r = fun x y => -x + y ∈ s
<VAR>α : Type u_1<VAR>Group α<VAR>s : Subgroup α<GOAL>Setoid.r = LeftCosetEquivalence ↑s
<VAR>α : Type u_1<VAR>Group α<VAR>s : Subgroup α<VAR>x y : α<GOAL>Setoid.r x y ↔ y * x⁻¹ ∈ s
<VAR>α : Type u_1<VAR>AddGroup α<VAR>s : AddSubgroup α<VAR>x y : α<GOAL>Setoid.r x y ↔ y + -x ∈ s
<VAR>α : Type u_1<VAR>Group α<VAR>s : Subgroup α<GOAL>Setoid.r = fun x y => y * x⁻¹ ∈ s
<VAR>α : Type u_1<VAR>AddGroup α<VAR>s : AddSubgroup α<GOAL>Setoid.r = fun x y => y + -x ∈ s
<VAR>α : Type u_1<VAR>Group α<VAR>s : Subgroup α<GOAL>Setoid.r = RightCosetEquivalence ↑s
<VAR>α : Type u_1<VAR>Group α<VAR>s : Subgroup α<VAR>Fintype (α ⧸ s)<GOAL>Fintype.card (Quotient (QuotientGroup.rightRel s)) = Fintype.card (α ⧸ s)
<VAR>α : Type u_1<VAR>AddGroup α<VAR>s : AddSubgroup α<VAR>Fintype (α ⧸ s)<GOAL>Fintype.card (Quotient (QuotientAddGroup.rightRel s)) = Fintype.card (α ⧸ s)
<VAR>α : Type u_1<VAR>AddGroup α<VAR>s : AddSubgroup α<GOAL>Function.Surjective QuotientAddGroup.mk
<VAR>α : Type u_1<VAR>Group α<VAR>s : Subgroup α<GOAL>Function.Surjective QuotientGroup.mk
<VAR>α : Type u_1<VAR>AddGroup α<VAR>s : AddSubgroup α<GOAL>Set.range QuotientAddGroup.mk = Set.univ
<VAR>α : Type u_1<VAR>Group α<VAR>s : Subgroup α<GOAL>Set.range QuotientGroup.mk = Set.univ
<VAR>α : Type u_1<VAR>AddGroup α<VAR>s : AddSubgroup α<VAR>C : α ⧸ s → Prop<VAR>x : α ⧸ s<VAR>H : ∀ (z : α), C ↑z<GOAL>C x
<VAR>α : Type u_1<VAR>Group α<VAR>s : Subgroup α<VAR>C : α ⧸ s → Prop<VAR>x : α ⧸ s<VAR>H : ∀ (z : α), C ↑z<GOAL>C x
<VAR>α : Type u_1<VAR>AddGroup α<VAR>s : AddSubgroup α<VAR>β : Sort u_2<VAR>f : α → β<VAR>h : ∀ (a b : α), Setoid.r a b → f a = f b<VAR>x : α<GOAL>Quotient.liftOn' (↑x) f h = f x
<VAR>α : Type u_1<VAR>Group α<VAR>s : Subgroup α<VAR>β : Sort u_2<VAR>f : α → β<VAR>h : ∀ (a b : α), Setoid.r a b → f a = f b<VAR>x : α<GOAL>Quotient.liftOn' (↑x) f h = f x
<VAR>α : Type u_1<VAR>Group α<VAR>s : Subgroup α<VAR>C : α ⧸ s → Prop<GOAL>(∀ (x : α ⧸ s), C x) ↔ ∀ (x : α), C ↑x
<VAR>α : Type u_1<VAR>AddGroup α<VAR>s : AddSubgroup α<VAR>C : α ⧸ s → Prop<GOAL>(∀ (x : α ⧸ s), C x) ↔ ∀ (x : α), C ↑x
<VAR>α : Type u_1<VAR>Group α<VAR>s : Subgroup α<VAR>C : α ⧸ s → Prop<GOAL>(∃ x, C x) ↔ ∃ x, C ↑x
<VAR>α : Type u_1<VAR>AddGroup α<VAR>s : AddSubgroup α<VAR>C : α ⧸ s → Prop<GOAL>(∃ x, C x) ↔ ∃ x, C ↑x
<VAR>α : Type u_1<VAR>AddGroup α<VAR>s : AddSubgroup α<VAR>a b : α<GOAL>↑a = ↑b ↔ -a + b ∈ s
<VAR>α : Type u_1<VAR>Group α<VAR>s : Subgroup α<VAR>a b : α<GOAL>↑a = ↑b ↔ a⁻¹ * b ∈ s
<VAR>α : Type u_1<VAR>Group α<VAR>s : Subgroup α<VAR>a : α ⧸ s<GOAL>↑(Quotient.out' a) = a
<VAR>α : Type u_1<VAR>AddGroup α<VAR>s : AddSubgroup α<VAR>a : α ⧸ s<GOAL>↑(Quotient.out' a) = a
<VAR>α : Type u_1<VAR>Group α<VAR>s : Subgroup α<VAR>g : α<GOAL>∃ h, Quotient.out' ↑g = g * ↑h
<VAR>α : Type u_1<VAR>AddGroup α<VAR>s : AddSubgroup α<VAR>g : α<GOAL>∃ h, Quotient.out' ↑g = g + ↑h
<VAR>α : Type u_1<VAR>Group α<VAR>s : Subgroup α<VAR>b : α<VAR>a : α<VAR>hb : b ∈ s<GOAL>↑(a * b) = ↑a
<VAR>α : Type u_1<VAR>AddGroup α<VAR>s : AddSubgroup α<VAR>b : α<VAR>a : α<VAR>hb : b ∈ s<GOAL>↑(a + b) = ↑a
<VAR>α : Type u_1<VAR>Group α<VAR>s : Subgroup α<VAR>g : α<GOAL>{x | ↑x = ↑g} = g • ↑s
<VAR>α : Type u_1<VAR>AddGroup α<VAR>s : AddSubgroup α<VAR>g : α<GOAL>{x | ↑x = ↑g} = g +ᵥ ↑s
<VAR>α : Type u_1<VAR>AddGroup α<VAR>N : AddSubgroup α<VAR>s : Set α<GOAL>QuotientAddGroup.mk ⁻¹' (QuotientAddGroup.mk '' s) = ⋃ x, (fun x_1 => x_1 + ↑x) ⁻¹' s
<VAR>α : Type u_1<VAR>Group α<VAR>N : Subgroup α<VAR>s : Set α<GOAL>QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' s) = ⋃ x, (fun x_1 => x_1 * ↑x) ⁻¹' s
<VAR>α : Type u_1<VAR>Group α<VAR>N : Subgroup α<VAR>s : Set α<GOAL>QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' s) = ⋃ x, (fun x_1 => x_1 * ↑x) '' s
<VAR>α : Type u_1<VAR>AddGroup α<VAR>N : AddSubgroup α<VAR>s : Set α<GOAL>QuotientAddGroup.mk ⁻¹' (QuotientAddGroup.mk '' s) = ⋃ x, (fun x_1 => x_1 + ↑x) '' s
<VAR>α : Type u_1<VAR>Group α<VAR>s t : Subgroup α<VAR>h : s = t<VAR>a : α<GOAL>(Subgroup.quotientEquivOfEq h) ↑a = ↑a
<VAR>α : Type u_1<VAR>AddGroup α<VAR>s t : AddSubgroup α<VAR>h_le : s ≤ t<VAR>f : α ⧸ t → α<VAR>hf : Function.RightInverse f QuotientAddGroup.mk<VAR>a : (α ⧸ t) × ↥t ⧸ s.addSubgroupOf t<GOAL>(AddSubgroup.quotientEquivSumOfLE' h_le f hf).symm a = Quotient.map' (fun b => f a.1 + ↑b) ⋯ a.2
<VAR>α : Type u_1<VAR>AddGroup α<VAR>s t : AddSubgroup α<VAR>h_le : s ≤ t<VAR>f : α ⧸ t → α<VAR>hf : Function.RightInverse f QuotientAddGroup.mk<VAR>a : α ⧸ s<GOAL>(AddSubgroup.quotientEquivSumOfLE' h_le f hf) a = (Quotient.map' id ⋯ a, Quotient.map' (fun g => ⟨-f (Quotient.mk'' g) + g, ⋯⟩) ⋯ a)
<VAR>α : Type u_1<VAR>Group α<VAR>s t : Subgroup α<VAR>h_le : s ≤ t<VAR>f : α ⧸ t → α<VAR>hf : Function.RightInverse f QuotientGroup.mk<VAR>a : (α ⧸ t) × ↥t ⧸ s.subgroupOf t<GOAL>(Subgroup.quotientEquivProdOfLE' h_le f hf).symm a = Quotient.map' (fun b => f a.1 * ↑b) ⋯ a.2
<VAR>α : Type u_1<VAR>Group α<VAR>s t : Subgroup α<VAR>h_le : s ≤ t<VAR>f : α ⧸ t → α<VAR>hf : Function.RightInverse f QuotientGroup.mk<VAR>a : α ⧸ s<GOAL>(Subgroup.quotientEquivProdOfLE' h_le f hf) a = (Quotient.map' id ⋯ a, Quotient.map' (fun g => ⟨(f (Quotient.mk'' g))⁻¹ * g, ⋯⟩) ⋯ a)
<VAR>α : Type u_1<VAR>AddGroup α<VAR>s t : AddSubgroup α<VAR>h_le : s ≤ t<VAR>a : (α ⧸ t) × ↥t ⧸ s.addSubgroupOf t<GOAL>(AddSubgroup.quotientEquivSumOfLE h_le).symm a = Quotient.map' (fun b => Quotient.out' a.1 + ↑b) ⋯ a.2
<VAR>α : Type u_1<VAR>AddGroup α<VAR>s t : AddSubgroup α<VAR>h_le : s ≤ t<VAR>a : α ⧸ s<GOAL>(AddSubgroup.quotientEquivSumOfLE h_le) a = (Quotient.map' id ⋯ a, Quotient.map' (fun g => ⟨-(Quotient.mk'' g).out' + g, ⋯⟩) ⋯ a)
<VAR>α : Type u_1<VAR>Group α<VAR>s t : Subgroup α<VAR>h_le : s ≤ t<VAR>a : (α ⧸ t) × ↥t ⧸ s.subgroupOf t<GOAL>(Subgroup.quotientEquivProdOfLE h_le).symm a = Quotient.map' (fun b => Quotient.out' a.1 * ↑b) ⋯ a.2
<VAR>α : Type u_1<VAR>Group α<VAR>s t : Subgroup α<VAR>h_le : s ≤ t<VAR>a : α ⧸ s<GOAL>(Subgroup.quotientEquivProdOfLE h_le) a = (Quotient.map' id ⋯ a, Quotient.map' (fun g => ⟨(Quotient.mk'' g).out'⁻¹ * g, ⋯⟩) ⋯ a)
<VAR>α : Type u_1<VAR>AddGroup α<VAR>s t : AddSubgroup α<VAR>H : AddSubgroup α<VAR>h : s ≤ t<VAR>g : ↥s<GOAL>(AddSubgroup.quotientAddSubgroupOfEmbeddingOfLE H h) ↑g = ↑((AddSubgroup.inclusion h) g)
<VAR>α : Type u_1<VAR>Group α<VAR>s t : Subgroup α<VAR>H : Subgroup α<VAR>h : s ≤ t<VAR>g : ↥s<GOAL>(Subgroup.quotientSubgroupOfEmbeddingOfLE H h) ↑g = ↑((Subgroup.inclusion h) g)
<VAR>α : Type u_1<VAR>Group α<VAR>s t : Subgroup α<VAR>H : Subgroup α<VAR>h : s ≤ t<VAR>g : ↥H<GOAL>Subgroup.quotientSubgroupOfMapOfLE H h ↑g = ↑g
<VAR>α : Type u_1<VAR>AddGroup α<VAR>s t : AddSubgroup α<VAR>H : AddSubgroup α<VAR>h : s ≤ t<VAR>g : ↥H<GOAL>AddSubgroup.quotientAddSubgroupOfMapOfLE H h ↑g = ↑g
<VAR>α : Type u_1<VAR>Group α<VAR>s t : Subgroup α<VAR>h : s ≤ t<VAR>g : α<GOAL>Subgroup.quotientMapOfLE h ↑g = ↑g
<VAR>α : Type u_1<VAR>AddGroup α<VAR>s t : AddSubgroup α<VAR>h : s ≤ t<VAR>g : α<GOAL>AddSubgroup.quotientMapOfLE h ↑g = ↑g
<VAR>α : Type u_1<VAR>Group α<VAR>ι : Type u_2<VAR>f : ι → Subgroup α<VAR>H : Subgroup α<VAR>q : ↥H ⧸ (⨅ i, f i).subgroupOf H<VAR>i : ι<GOAL>(Subgroup.quotientiInfSubgroupOfEmbedding f H) q i = Subgroup.quotientSubgroupOfMapOfLE H ⋯ q
<VAR>α : Type u_1<VAR>AddGroup α<VAR>ι : Type u_2<VAR>f : ι → AddSubgroup α<VAR>H : AddSubgroup α<VAR>q : ↥H ⧸ (⨅ i, f i).addSubgroupOf H<VAR>i : ι<GOAL>(AddSubgroup.quotientiInfAddSubgroupOfEmbedding f H) q i = AddSubgroup.quotientAddSubgroupOfMapOfLE H ⋯ q
<VAR>α : Type u_1<VAR>Group α<VAR>ι : Type u_2<VAR>f : ι → Subgroup α<VAR>H : Subgroup α<VAR>g : ↥H<VAR>i : ι<GOAL>(Subgroup.quotientiInfSubgroupOfEmbedding f H) (↑g) i = ↑g
<VAR>α : Type u_1<VAR>AddGroup α<VAR>ι : Type u_2<VAR>f : ι → AddSubgroup α<VAR>H : AddSubgroup α<VAR>g : ↥H<VAR>i : ι<GOAL>(AddSubgroup.quotientiInfAddSubgroupOfEmbedding f H) (↑g) i = ↑g
<VAR>α : Type u_1<VAR>Group α<VAR>ι : Type u_2<VAR>f : ι → Subgroup α<VAR>q : α ⧸ ⨅ i, f i<VAR>i : ι<GOAL>(Subgroup.quotientiInfEmbedding f) q i = Subgroup.quotientMapOfLE ⋯ q
<VAR>α : Type u_1<VAR>AddGroup α<VAR>ι : Type u_2<VAR>f : ι → AddSubgroup α<VAR>q : α ⧸ ⨅ i, f i<VAR>i : ι<GOAL>(AddSubgroup.quotientiInfEmbedding f) q i = AddSubgroup.quotientMapOfLE ⋯ q
<VAR>α : Type u_1<VAR>AddGroup α<VAR>ι : Type u_2<VAR>f : ι → AddSubgroup α<VAR>g : α<VAR>i : ι<GOAL>(AddSubgroup.quotientiInfEmbedding f) (↑g) i = ↑g
<VAR>α : Type u_1<VAR>Group α<VAR>ι : Type u_2<VAR>f : ι → Subgroup α<VAR>g : α<VAR>i : ι<GOAL>(Subgroup.quotientiInfEmbedding f) (↑g) i = ↑g
<VAR>α : Type u_1<VAR>AddGroup α<VAR>s : AddSubgroup α<GOAL>Nat.card α = Nat.card (α ⧸ s) * Nat.card ↥s
<VAR>α : Type u_1<VAR>Group α<VAR>s : Subgroup α<GOAL>Nat.card α = Nat.card (α ⧸ s) * Nat.card ↥s
<VAR>α : Type u_1<VAR>AddGroup α<VAR>s : AddSubgroup α<GOAL>Nat.card ↥s ∣ Nat.card α
<VAR>α : Type u_1<VAR>Group α<VAR>s : Subgroup α<GOAL>Nat.card ↥s ∣ Nat.card α
<VAR>α : Type u_1<VAR>AddGroup α<VAR>s : AddSubgroup α<GOAL>Nat.card (α ⧸ s) ∣ Nat.card α
<VAR>α : Type u_1<VAR>Group α<VAR>s : Subgroup α<GOAL>Nat.card (α ⧸ s) ∣ Nat.card α
<VAR>α : Type u_1<VAR>AddGroup α<VAR>H : Type u_2<VAR>AddGroup H<VAR>f : α →+ H<VAR>hf : Function.Injective ⇑f<GOAL>Nat.card α ∣ Nat.card H
<VAR>α : Type u_1<VAR>Group α<VAR>H : Type u_2<VAR>Group H<VAR>f : α →* H<VAR>hf : Function.Injective ⇑f<GOAL>Nat.card α ∣ Nat.card H
<VAR>α : Type u_1<VAR>AddGroup α<VAR>H K : AddSubgroup α<VAR>hHK : H ≤ K<GOAL>Nat.card ↥H ∣ Nat.card ↥K
<VAR>α : Type u_1<VAR>Group α<VAR>H K : Subgroup α<VAR>hHK : H ≤ K<GOAL>Nat.card ↥H ∣ Nat.card ↥K
<VAR>α : Type u_1<VAR>Group α<VAR>H : Type u_2<VAR>Group H<VAR>K : Subgroup H<VAR>f : α →* H<VAR>hf : Function.Injective ⇑f<GOAL>Nat.card ↥(Subgroup.comap f K) ∣ Nat.card ↥K
<VAR>α : Type u_1<VAR>AddGroup α<VAR>H : Type u_2<VAR>AddGroup H<VAR>K : AddSubgroup H<VAR>f : α →+ H<VAR>hf : Function.Injective ⇑f<GOAL>Nat.card ↥(AddSubgroup.comap f K) ∣ Nat.card ↥K
<VAR>α : Type u_1<VAR>Group α<VAR>H : Type u_2<VAR>Group H<VAR>f : α →* H<VAR>a : α<VAR>g : ↑(⇑f ⁻¹' {f a})<GOAL>↑((f.fiberEquivKer a) g) = a⁻¹ * ↑g
<VAR>α : Type u_1<VAR>AddGroup α<VAR>H : Type u_2<VAR>AddGroup H<VAR>f : α →+ H<VAR>a : α<VAR>g : ↑(⇑f ⁻¹' {f a})<GOAL>↑((f.fiberEquivKer a) g) = -a + ↑g
<VAR>α : Type u_1<VAR>AddGroup α<VAR>H : Type u_2<VAR>AddGroup H<VAR>f : α →+ H<VAR>a : α<VAR>g : ↥f.ker<GOAL>↑((f.fiberEquivKer a).symm g) = a + ↑g
<VAR>α : Type u_1<VAR>Group α<VAR>H : Type u_2<VAR>Group H<VAR>f : α →* H<VAR>a : α<VAR>g : ↥f.ker<GOAL>↑((f.fiberEquivKer a).symm g) = a * ↑g
<VAR>α : Type u_1<VAR>Group α<VAR>H : Type u_2<VAR>Group H<VAR>f : α →* H<VAR>a b : α<VAR>g : ↑(⇑f ⁻¹' {f a})<GOAL>↑((f.fiberEquiv a b) g) = b * (a⁻¹ * ↑g)
<VAR>α : Type u_1<VAR>AddGroup α<VAR>H : Type u_2<VAR>AddGroup H<VAR>f : α →+ H<VAR>a b : α<VAR>g : ↑(⇑f ⁻¹' {f a})<GOAL>↑((f.fiberEquiv a b) g) = b + (-a + ↑g)
<VAR>α : Type u_1<VAR>AddGroup α<VAR>H : Type u_2<VAR>AddGroup H<VAR>f : α →+ H<VAR>a b : α<VAR>g : ↑(⇑f ⁻¹' {f b})<GOAL>↑((f.fiberEquiv a b).symm g) = a + (-b + ↑g)
<VAR>α : Type u_1<VAR>Group α<VAR>H : Type u_2<VAR>Group H<VAR>f : α →* H<VAR>a b : α<VAR>g : ↑(⇑f ⁻¹' {f b})<GOAL>↑((f.fiberEquiv a b).symm g) = a * (b⁻¹ * ↑g)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>f : ι → G<VAR>comm : (↑s).Pairwise fun a b => AddCommute (f a) (f b)<VAR>K : ι → AddSubgroup G<VAR>hind : CompleteLattice.Independent K<VAR>hmem : ∀ x ∈ s, f x ∈ K x<VAR>heq1 : s.noncommSum f comm = 0<VAR>i : ι<GOAL>i ∈ s → f i = 0
<VAR>G : Type u_1<VAR>Group G<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>f : ι → G<VAR>comm : (↑s).Pairwise fun a b => Commute (f a) (f b)<VAR>K : ι → Subgroup G<VAR>hind : CompleteLattice.Independent K<VAR>hmem : ∀ x ∈ s, f x ∈ K x<VAR>heq1 : s.noncommProd f comm = 1<VAR>i : ι<GOAL>i ∈ s → f i = 1
<VAR>M : Type u_1<VAR>Monoid M<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>Fintype ι<VAR>N : ι → Type u_3<VAR>(i : ι) → Monoid (N i)<VAR>ϕ : (i : ι) → N i →* M<VAR>hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)<VAR>i : ι<VAR>y : N i<GOAL>(MonoidHom.noncommPiCoprod ϕ hcomm) (Pi.mulSingle i y) = (ϕ i) y
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>Fintype ι<VAR>N : ι → Type u_3<VAR>(i : ι) → AddMonoid (N i)<VAR>ϕ : (i : ι) → N i →+ M<VAR>hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), AddCommute ((ϕ i) x) ((ϕ j) y)<VAR>i : ι<VAR>y : N i<GOAL>(AddMonoidHom.noncommPiCoprod ϕ hcomm) (Pi.single i y) = (ϕ i) y
<VAR>M : Type u_1<VAR>Monoid M<VAR>ι : Type u_2<VAR>Fintype ι<VAR>N : ι → Type u_3<VAR>(i : ι) → Monoid (N i)<VAR>ϕ : (i : ι) → N i →* M<VAR>hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)<GOAL>MonoidHom.mrange (MonoidHom.noncommPiCoprod ϕ hcomm) = ⨆ i, MonoidHom.mrange (ϕ i)
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>ι : Type u_2<VAR>Fintype ι<VAR>N : ι → Type u_3<VAR>(i : ι) → AddMonoid (N i)<VAR>ϕ : (i : ι) → N i →+ M<VAR>hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), AddCommute ((ϕ i) x) ((ϕ j) y)<GOAL>AddMonoidHom.mrange (AddMonoidHom.noncommPiCoprod ϕ hcomm) = ⨆ i, AddMonoidHom.mrange (ϕ i)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>ι : Type u_2<VAR>hfin : Fintype ι<VAR>H : ι → Type u_3<VAR>(i : ι) → AddGroup (H i)<VAR>ϕ : (i : ι) → H i →+ G<VAR>hcomm : Pairwise fun i j => ∀ (x : H i) (y : H j), AddCommute ((ϕ i) x) ((ϕ j) y)<GOAL>(AddMonoidHom.noncommPiCoprod ϕ hcomm).range = ⨆ i, (ϕ i).range
<VAR>G : Type u_1<VAR>Group G<VAR>ι : Type u_2<VAR>hfin : Fintype ι<VAR>H : ι → Type u_3<VAR>(i : ι) → Group (H i)<VAR>ϕ : (i : ι) → H i →* G<VAR>hcomm : Pairwise fun i j => ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)<GOAL>(MonoidHom.noncommPiCoprod ϕ hcomm).range = ⨆ i, (ϕ i).range
<VAR>G : Type u_1<VAR>AddGroup G<VAR>ι : Type u_2<VAR>hfin : Fintype ι<VAR>H : ι → Type u_3<VAR>(i : ι) → AddGroup (H i)<VAR>ϕ : (i : ι) → H i →+ G<VAR>hcomm : Pairwise fun i j => ∀ (x : H i) (y : H j), AddCommute ((ϕ i) x) ((ϕ j) y)<VAR>hind : CompleteLattice.Independent fun i => (ϕ i).range<VAR>hinj : ∀ (i : ι), Function.Injective ⇑(ϕ i)<GOAL>Function.Injective ⇑(AddMonoidHom.noncommPiCoprod ϕ hcomm)
<VAR>G : Type u_1<VAR>Group G<VAR>ι : Type u_2<VAR>hfin : Fintype ι<VAR>H : ι → Type u_3<VAR>(i : ι) → Group (H i)<VAR>ϕ : (i : ι) → H i →* G<VAR>hcomm : Pairwise fun i j => ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)<VAR>hind : CompleteLattice.Independent fun i => (ϕ i).range<VAR>hinj : ∀ (i : ι), Function.Injective ⇑(ϕ i)<GOAL>Function.Injective ⇑(MonoidHom.noncommPiCoprod ϕ hcomm)
<VAR>G : Type u_1<VAR>Group G<VAR>ι : Type u_2<VAR>H : ι → Type u_3<VAR>(i : ι) → Group (H i)<VAR>ϕ : (i : ι) → H i →* G<VAR>hcomm : Pairwise fun i j => ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)<VAR>Finite ι<VAR>(i : ι) → Fintype (H i)<VAR>hcoprime : Pairwise fun i j => (Fintype.card (H i)).Coprime (Fintype.card (H j))<GOAL>CompleteLattice.Independent fun i => (ϕ i).range
<VAR>G : Type u_1<VAR>AddGroup G<VAR>ι : Type u_2<VAR>H : ι → Type u_3<VAR>(i : ι) → AddGroup (H i)<VAR>ϕ : (i : ι) → H i →+ G<VAR>hcomm : Pairwise fun i j => ∀ (x : H i) (y : H j), AddCommute ((ϕ i) x) ((ϕ j) y)<VAR>Finite ι<VAR>(i : ι) → Fintype (H i)<VAR>hcoprime : Pairwise fun i j => (Fintype.card (H i)).Coprime (Fintype.card (H j))<GOAL>CompleteLattice.Independent fun i => (ϕ i).range
<VAR>G : Type u_1<VAR>AddGroup G<VAR>ι : Type u_2<VAR>H : ι → AddSubgroup G<VAR>hcomm : Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → AddCommute x y<VAR>i j : ι<VAR>hne : i ≠ j<VAR>x : ↥(H i)<VAR>y : ↥(H j)<GOAL>AddCommute ((H i).subtype x) ((H j).subtype y)
<VAR>G : Type u_1<VAR>Group G<VAR>ι : Type u_2<VAR>H : ι → Subgroup G<VAR>hcomm : Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y<VAR>i j : ι<VAR>hne : i ≠ j<VAR>x : ↥(H i)<VAR>y : ↥(H j)<GOAL>Commute ((H i).subtype x) ((H j).subtype y)
<VAR>G : Type u_1<VAR>Group G<VAR>ι : Type u_2<VAR>hdec : DecidableEq ι<VAR>hfin : Fintype ι<VAR>H : ι → Subgroup G<VAR>hcomm : Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y<VAR>i : ι<VAR>y : ↥(H i)<GOAL>(Subgroup.noncommPiCoprod hcomm) (Pi.mulSingle i y) = ↑y
<VAR>G : Type u_1<VAR>AddGroup G<VAR>ι : Type u_2<VAR>hdec : DecidableEq ι<VAR>hfin : Fintype ι<VAR>H : ι → AddSubgroup G<VAR>hcomm : Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → AddCommute x y<VAR>i : ι<VAR>y : ↥(H i)<GOAL>(AddSubgroup.noncommPiCoprod hcomm) (Pi.single i y) = ↑y
<VAR>G : Type u_1<VAR>Group G<VAR>ι : Type u_2<VAR>hfin : Fintype ι<VAR>H : ι → Subgroup G<VAR>hcomm : Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y<GOAL>(Subgroup.noncommPiCoprod hcomm).range = ⨆ i, H i
<VAR>G : Type u_1<VAR>AddGroup G<VAR>ι : Type u_2<VAR>hfin : Fintype ι<VAR>H : ι → AddSubgroup G<VAR>hcomm : Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → AddCommute x y<GOAL>(AddSubgroup.noncommPiCoprod hcomm).range = ⨆ i, H i
<VAR>G : Type u_1<VAR>Group G<VAR>ι : Type u_2<VAR>hfin : Fintype ι<VAR>H : ι → Subgroup G<VAR>hcomm : Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y<VAR>hind : CompleteLattice.Independent H<GOAL>Function.Injective ⇑(Subgroup.noncommPiCoprod hcomm)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>ι : Type u_2<VAR>hfin : Fintype ι<VAR>H : ι → AddSubgroup G<VAR>hcomm : Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → AddCommute x y<VAR>hind : CompleteLattice.Independent H<GOAL>Function.Injective ⇑(AddSubgroup.noncommPiCoprod hcomm)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>ι : Type u_2<VAR>H : ι → AddSubgroup G<VAR>hcomm : Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → AddCommute x y<VAR>Finite ι<VAR>(i : ι) → Fintype ↥(H i)<VAR>hcoprime : Pairwise fun i j => (Fintype.card ↥(H i)).Coprime (Fintype.card ↥(H j))<GOAL>CompleteLattice.Independent H
<VAR>G : Type u_1<VAR>Group G<VAR>ι : Type u_2<VAR>H : ι → Subgroup G<VAR>hcomm : Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y<VAR>Finite ι<VAR>(i : ι) → Fintype ↥(H i)<VAR>hcoprime : Pairwise fun i j => (Fintype.card ↥(H i)).Coprime (Fintype.card ↥(H j))<GOAL>CompleteLattice.Independent H
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>VAdd G α<VAR>s : Set α<VAR>a : α<VAR>ha : a ∈ s<GOAL>AddAction.Supports G s a
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>SMul G α<VAR>s : Set α<VAR>a : α<VAR>ha : a ∈ s<GOAL>MulAction.Supports G s a
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>VAdd G α<VAR>VAdd G β<VAR>s t : Set α<VAR>b : β<VAR>h : s ⊆ t<VAR>hs : AddAction.Supports G s b<GOAL>AddAction.Supports G t b
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>SMul G α<VAR>SMul G β<VAR>s t : Set α<VAR>b : β<VAR>h : s ⊆ t<VAR>hs : MulAction.Supports G s b<GOAL>MulAction.Supports G t b
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddGroup H<VAR>VAdd G α<VAR>VAdd G β<VAR>AddAction H α<VAR>VAdd H β<VAR>VAddCommClass G H β<VAR>VAddCommClass G H α<VAR>s : Set α<VAR>b : β<VAR>g : H<VAR>h : AddAction.Supports G s b<GOAL>AddAction.Supports G (g +ᵥ s) (g +ᵥ b)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Group H<VAR>SMul G α<VAR>SMul G β<VAR>MulAction H α<VAR>SMul H β<VAR>SMulCommClass G H β<VAR>SMulCommClass G H α<VAR>s : Set α<VAR>b : β<VAR>g : H<VAR>h : MulAction.Supports G s b<GOAL>MulAction.Supports G (g • s) (g • b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddMonoid β<VAR>DistribSMul α β<VAR>r : α<VAR>l : List β<GOAL>r • l.sum = (List.map (fun x => r • x) l).sum
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Monoid α<VAR>Monoid β<VAR>MulDistribMulAction α β<VAR>r : α<VAR>l : List β<GOAL>r • l.prod = (List.map (fun x => r • x) l).prod
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid β<VAR>DistribSMul α β<VAR>r : α<VAR>s : Multiset β<GOAL>r • s.sum = (Multiset.map (fun x => r • x) s).sum
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>AddCommMonoid β<VAR>DistribSMul α β<VAR>r : α<VAR>f : γ → β<VAR>s : Finset γ<GOAL>r • ∑ x ∈ s, f x = ∑ x ∈ s, r • f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Monoid α<VAR>CommMonoid β<VAR>MulDistribMulAction α β<VAR>r : α<VAR>s : Multiset β<GOAL>r • s.prod = (Multiset.map (fun x => r • x) s).prod
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Monoid α<VAR>CommMonoid β<VAR>MulDistribMulAction α β<VAR>r : α<VAR>f : γ → β<VAR>s : Finset γ<GOAL>r • ∏ x ∈ s, f x = ∏ x ∈ s, r • f x
<VAR>A : Type u_1<VAR>α : Type u_2<VAR>AddMonoid A<VAR>SMul α A<VAR>Zero α<VAR>self : DivisibleBy A α<VAR>a : A<GOAL>DivisibleBy.div a 0 = 0
<VAR>A : Type u_1<VAR>α : Type u_2<VAR>AddMonoid A<VAR>SMul α A<VAR>Zero α<VAR>self : DivisibleBy A α<VAR>n : α<VAR>a : A<GOAL>n ≠ 0 → n • DivisibleBy.div a n = a
<VAR>A : Type u_1<VAR>α : Type u_2<VAR>Monoid A<VAR>Pow A α<VAR>Zero α<VAR>self : RootableBy A α<VAR>a : A<GOAL>RootableBy.root a 0 = 1
<VAR>A : Type u_1<VAR>α : Type u_2<VAR>Monoid A<VAR>Pow A α<VAR>Zero α<VAR>self : RootableBy A α<VAR>n : α<VAR>a : A<GOAL>n ≠ 0 → RootableBy.root a n ^ n = a
<VAR>A : Type u_1<VAR>α : Type u_2<VAR>Monoid A<VAR>Pow A α<VAR>Zero α<VAR>RootableBy A α<VAR>n : α<VAR>hn : n ≠ 0<GOAL>Function.Surjective fun a => a ^ n
<VAR>A : Type u_1<VAR>α : Type u_2<VAR>AddMonoid A<VAR>SMul α A<VAR>Zero α<VAR>DivisibleBy A α<VAR>n : α<VAR>hn : n ≠ 0<GOAL>Function.Surjective fun a => n • a
<VAR>A : Type u_1<VAR>AddCommGroup A<VAR>DivisibleBy A ℤ<VAR>n : ℤ<VAR>hn : n ≠ 0<GOAL>n • ⊤ = ⊤
<VAR>A : Type u_4<VAR>α : Type u_5<VAR>Monoid A<VAR>Pow A α<VAR>Zero α<VAR>RootableBy A α<VAR>n : α<VAR>hn : n ≠ 0<GOAL>Function.Surjective fun a => a ^ n
<VAR>A : Type u_4<VAR>α : Type u_5<VAR>AddMonoid A<VAR>SMul α A<VAR>Zero α<VAR>DivisibleBy A α<VAR>n : α<VAR>hn : n ≠ 0<GOAL>Function.Surjective fun a => n • a
<VAR>G : Type u<VAR>Monoid G<GOAL>AddMonoid.exponent (Additive G) = Monoid.exponent G
<VAR>G : Type u_1<VAR>AddMonoid G<GOAL>Monoid.exponent (Multiplicative G) = AddMonoid.exponent G
<VAR>G : Type u<VAR>AddMonoid G<GOAL>AddMonoid.exponent Gᵃᵒᵖ = AddMonoid.exponent G
<VAR>G : Type u<VAR>Monoid G<GOAL>Monoid.exponent Gᵐᵒᵖ = Monoid.exponent G
<VAR>G : Type u<VAR>AddMonoid G<VAR>h : AddMonoid.ExponentExists G<VAR>g : G<GOAL>IsOfFinAddOrder g
<VAR>G : Type u<VAR>Monoid G<VAR>h : Monoid.ExponentExists G<VAR>g : G<GOAL>IsOfFinOrder g