internlm/Lean-Github huggingface dataset:
Theorem: Finset.mulStab_quotient_commute_subgroup
Proof state before:
case inr.a.mpr.intro.intro.intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
ht : t.Nonempty
hti : (image QuotientGroup.mk t).Nonempty
x : α ⧸ s
y : α
hyx : ⟦y⟧ = x
z : α
hzt : z ∈ t
hx : image QuotientGroup.mk (y • t) = image QuotientGroup.mk t
b : α
hbt : b ∈ t
ha : y • b ∈ y • t
hayz : (y * b)⁻¹ * z ∈ s
c : α
hct : c ∈ t.mulStab
hcbyz : (y • b)⁻¹ * z = c
⊢ z ∈ y • t
Tactic:
rw [inv_mul_eq_iff_eq_mul] at hcbyz
Proof state after:
case inr.a.mpr.intro.intro.intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
ht : t.Nonempty
hti : (image QuotientGroup.mk t).Nonempty
x : α ⧸ s
y : α
hyx : ⟦y⟧ = x
z : α
hzt : z ∈ t
hx : image QuotientGroup.mk (y • t) = image QuotientGroup.mk t
b : α
hbt : b ∈ t
ha : y • b ∈ y • t
hayz : (y * b)⁻¹ * z ∈ s
c : α
hct : c ∈ t.mulStab
hcbyz : z = y • b * c
⊢ z ∈ y • t
Theorem: Finset.mulStab_quotient_commute_subgroup
Proof state before:
case inr.a.mpr.intro.intro.intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
ht : t.Nonempty
hti : (image QuotientGroup.mk t).Nonempty
x : α ⧸ s
y : α
hyx : ⟦y⟧ = x
z : α
hzt : z ∈ t
hx : image QuotientGroup.mk (y • t) = image QuotientGroup.mk t
b : α
hbt : b ∈ t
ha : y • b ∈ y • t
hayz : (y * b)⁻¹ * z ∈ s
c : α
hct : c ∈ t.mulStab
hcbyz : z = y • b * c
⊢ z ∈ y • t
Tactic:
rw [hcbyz, smul_mul_assoc, mul_comm, ← smul_eq_mul]
Proof state after:
case inr.a.mpr.intro.intro.intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
ht : t.Nonempty
hti : (image QuotientGroup.mk t).Nonempty
x : α ⧸ s
y : α
hyx : ⟦y⟧ = x
z : α
hzt : z ∈ t
hx : image QuotientGroup.mk (y • t) = image QuotientGroup.mk t
b : α
hbt : b ∈ t
ha : y • b ∈ y • t
hayz : (y * b)⁻¹ * z ∈ s
c : α
hct : c ∈ t.mulStab
hcbyz : z = y • b * c
⊢ y • c • b ∈ y • t
Theorem: Finset.mulStab_quotient_commute_subgroup
Proof state before:
case inr.a.mpr.intro.intro.intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
ht : t.Nonempty
hti : (image QuotientGroup.mk t).Nonempty
x : α ⧸ s
y : α
hyx : ⟦y⟧ = x
z : α
hzt : z ∈ t
hx : image QuotientGroup.mk (y • t) = image QuotientGroup.mk t
b : α
hbt : b ∈ t
ha : y • b ∈ y • t
hayz : (y * b)⁻¹ * z ∈ s
c : α
hct : c ∈ t.mulStab
hcbyz : z = y • b * c
⊢ y • c • b ∈ y • t
Tactic:
exact smul_mem_smul_finset ((mem_mulStab' ht).mp hct hbt)
Proof state after:
no goals
Theorem: Finset.mulStab_quotient_commute_subgroup
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
ht : t.Nonempty
hti : (image QuotientGroup.mk t).Nonempty
x : α ⧸ s
hx : x • image QuotientGroup.mk t = image QuotientGroup.mk t
⊢ s ≤ stabilizer α t
Tactic:
aesop
Proof state after:
no goals
Theorem: Finset.mulStab_quotient_commute_subgroup
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
ht : t.Nonempty
hti : (image QuotientGroup.mk t).Nonempty
x : α ⧸ s
hx : x • image QuotientGroup.mk t = image QuotientGroup.mk t
this : s ≤ stabilizer α t
y : α
hyx : ⟦y⟧ = x
⊢ ↑y = x
Tactic:
simpa
Proof state after:
no goals
Theorem: Finset.mulStab_quotient_commute_subgroup
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
ht : t.Nonempty
hti : (image QuotientGroup.mk t).Nonempty
x : α ⧸ s
hx : x • image QuotientGroup.mk t = image QuotientGroup.mk t
this : s ≤ stabilizer α t
y : α
hyx : ⟦y⟧ = x
z : α
hzt : z ∈ t
⊢ image QuotientGroup.mk (y • t) = image QuotientGroup.mk t
Tactic:
rw [← hx, ← hyx]
Proof state after:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
ht : t.Nonempty
hti : (image QuotientGroup.mk t).Nonempty
x : α ⧸ s
hx : x • image QuotientGroup.mk t = image QuotientGroup.mk t
this : s ≤ stabilizer α t
y : α
hyx : ⟦y⟧ = x
z : α
hzt : z ∈ t
⊢ image QuotientGroup.mk (y • t) = ⟦y⟧ • image QuotientGroup.mk t
Theorem: Finset.mulStab_quotient_commute_subgroup
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
ht : t.Nonempty
hti : (image QuotientGroup.mk t).Nonempty
x : α ⧸ s
hx : x • image QuotientGroup.mk t = image QuotientGroup.mk t
this : s ≤ stabilizer α t
y : α
hyx : ⟦y⟧ = x
z : α
hzt : z ∈ t
⊢ image QuotientGroup.mk (y • t) = ⟦y⟧ • image QuotientGroup.mk t
Tactic:
exact image_smul_comm QuotientGroup.mk y t (congrFun rfl)
Proof state after:
no goals
Theorem: Finset.mulStab_quotient_commute_subgroup
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
ht : t.Nonempty
hti : (image QuotientGroup.mk t).Nonempty
x : α ⧸ s
this : s ≤ stabilizer α t
y : α
hyx : ⟦y⟧ = x
z : α
hzt : z ∈ t
hx : image QuotientGroup.mk (y • t) = image QuotientGroup.mk t
⊢ ↑z ∈ image QuotientGroup.mk (y • t)
Tactic:
aesop
Proof state after:
no goals
Theorem: Finset.mulStab_quotient_commute_subgroup
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
ht : t.Nonempty
hti : (image QuotientGroup.mk t).Nonempty
x : α ⧸ s
this : s ≤ stabilizer α t
y : α
hyx : ⟦y⟧ = x
z : α
hzt : z ∈ t
hx : image QuotientGroup.mk (y • t) = image QuotientGroup.mk t
b : α
hbt : b ∈ t
ha : y • b ∈ y • t
hayz : (y * b)⁻¹ * z ∈ s
⊢ ∃ c ∈ t.mulStab, (y • b)⁻¹ * z = c
Tactic:
aesop
Proof state after:
no goals
Theorem: Finset.mul_prod_Ico
Proof state before:
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : CommMonoid β
f : α → β
a b : α
inst✝ : LocallyFiniteOrder α
h : a ≤ b
⊢ f b * ∏ x ∈ Ico a b, f x = ∏ x ∈ Icc a b, f x
Tactic:
rw [Icc_eq_cons_Ico h, prod_cons]
Proof state after:
no goals
Theorem: Finset.mul_prod_Ioc
Proof state before:
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : CommMonoid β
f : α → β
a b : α
inst✝ : LocallyFiniteOrder α
h : a ≤ b
⊢ f a * ∏ x ∈ Ioc a b, f x = ∏ x ∈ Icc a b, f x
Tactic:
rw [Icc_eq_cons_Ioc h, prod_cons]
Proof state after:
no goals
Theorem: Finset.mul_prod_Ioi
Proof state before:
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : CommMonoid β
f : α → β
a✝ b : α
inst✝ : LocallyFiniteOrderTop α
a : α
⊢ f a * ∏ x ∈ Ioi a, f x = ∏ x ∈ Ici a, f x
Tactic:
rw [Ici_eq_cons_Ioi, prod_cons]
Proof state after:
no goals
Theorem: Finset.mul_prod_Iio
Proof state before:
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : CommMonoid β
f : α → β
a✝ b : α
inst✝ : LocallyFiniteOrderBot α
a : α
⊢ f a * ∏ x ∈ Iio a, f x = ∏ x ∈ Iic a, f x
Tactic:
rw [Iic_eq_cons_Iio, prod_cons]
Proof state after:
no goals
Theorem: Finpartition.multipartiteGraph_adj_of_mem_parts
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
P : Finpartition univ
s t : Finset α
a b : α
hs : s ∈ P.parts
ht : t ∈ P.parts
ha : a ∈ s
hb : b ∈ t
⊢ P.multipartiteGraph.Adj a b ↔ s ≠ t
Tactic:
refine' ⟨_, fun hst u hu hau hbu => hst _⟩
Proof state after:
case refine'_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
P : Finpartition univ
s t : Finset α
a b : α
hs : s ∈ P.parts
ht : t ∈ P.parts
ha : a ∈ s
hb : b ∈ t
⊢ P.multipartiteGraph.Adj a b → s ≠ t

case refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
P : Finpartition univ
s t : Finset α
a b : α
hs : s ∈ P.parts
ht : t ∈ P.parts
ha : a ∈ s
hb : b ∈ t
hst : s ≠ t
u : Finset α
hu : u ∈ P.parts
hau : a ∈ u
hbu : b ∈ u
⊢ s = t
Theorem: Finpartition.multipartiteGraph_adj_of_mem_parts
Proof state before:
case refine'_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
P : Finpartition univ
s t : Finset α
a b : α
hs : s ∈ P.parts
ht : t ∈ P.parts
ha : a ∈ s
hb : b ∈ t
⊢ P.multipartiteGraph.Adj a b → s ≠ t
Tactic:
rintro hab rfl
Proof state after:
case refine'_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
P : Finpartition univ
s : Finset α
a b : α
hs : s ∈ P.parts
ha : a ∈ s
hab : P.multipartiteGraph.Adj a b
ht : s ∈ P.parts
hb : b ∈ s
⊢ False
Theorem: Finpartition.multipartiteGraph_adj_of_mem_parts
Proof state before:
case refine'_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
P : Finpartition univ
s : Finset α
a b : α
hs : s ∈ P.parts
ha : a ∈ s
hab : P.multipartiteGraph.Adj a b
ht : s ∈ P.parts
hb : b ∈ s
⊢ False
Tactic:
exact hab hs ha hb
Proof state after:
no goals
Theorem: Finpartition.multipartiteGraph_adj_of_mem_parts
Proof state before:
case refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
P : Finpartition univ
s t : Finset α
a b : α
hs : s ∈ P.parts
ht : t ∈ P.parts
ha : a ∈ s
hb : b ∈ t
hst : s ≠ t
u : Finset α
hu : u ∈ P.parts
hau : a ∈ u
hbu : b ∈ u
⊢ s = t
Tactic:
rw [P.eq_of_mem_parts hs hu ha hau, P.eq_of_mem_parts ht hu hb hbu]
Proof state after:
no goals
Theorem: Subgroup.coe_eq_one
Proof state before:
α : Type u_1
inst✝ : Group α
s : Subgroup α
a : α
⊢ ↑s = ↑⊥ ↔ ↑s = 1
Tactic:
rfl
Proof state after:
no goals
Theorem: Subgroup.smul_coe
Proof state before:
α : Type u_1
inst✝ : Group α
s : Subgroup α
a : α
ha : a ∈ s
⊢ a • ↑s = ↑s
Tactic:
ext
Proof state after:
case h
α : Type u_1
inst✝ : Group α
s : Subgroup α
a : α
ha : a ∈ s
x✝ : α
⊢ x✝ ∈ a • ↑s ↔ x✝ ∈ ↑s
Theorem: Subgroup.smul_coe
Proof state before:
case h
α : Type u_1
inst✝ : Group α
s : Subgroup α
a : α
ha : a ∈ s
x✝ : α
⊢ x✝ ∈ a • ↑s ↔ x✝ ∈ ↑s
Tactic:
rw [Set.mem_smul_set_iff_inv_smul_mem]
Proof state after:
case h
α : Type u_1
inst✝ : Group α
s : Subgroup α
a : α
ha : a ∈ s
x✝ : α
⊢ a⁻¹ • x✝ ∈ ↑s ↔ x✝ ∈ ↑s
Theorem: Subgroup.smul_coe
Proof state before:
case h
α : Type u_1
inst✝ : Group α
s : Subgroup α
a : α
ha : a ∈ s
x✝ : α
⊢ a⁻¹ • x✝ ∈ ↑s ↔ x✝ ∈ ↑s
Tactic:
exact Subgroup.mul_mem_cancel_left _ (inv_mem ha)
Proof state after:
no goals
Theorem: Subgroup.subgroup_mul_card_eq_mul
Proof state before:
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
⊢ Nat.card ↥s * Nat.card ↑(QuotientGroup.mk '' t) = Nat.card ↑(t * ↑s)
Tactic:
rw [← Nat.card_prod, Nat.card_congr]
Proof state after:
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
⊢ ↥s × ↑(QuotientGroup.mk '' t) ≃ ↑(t * ↑s)
Theorem: Subgroup.subgroup_mul_card_eq_mul
Proof state before:
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
⊢ ↥s × ↑(QuotientGroup.mk '' t) ≃ ↑(t * ↑s)
Tactic:
apply Equiv.trans (QuotientGroup.preimageMkEquivSubgroupProdSet _ _).symm
Proof state after:
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
⊢ ↑(QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' t)) ≃ ↑(t * ↑s)
Theorem: Subgroup.subgroup_mul_card_eq_mul
Proof state before:
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
⊢ ↑(QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' t)) ≃ ↑(t * ↑s)
Tactic:
rw [QuotientGroup.preimage_image_mk]
Proof state after:
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
⊢ ↑(⋃ x, (fun x_1 => x_1 * ↑x) ⁻¹' t) ≃ ↑(t * ↑s)
Theorem: Subgroup.subgroup_mul_card_eq_mul
Proof state before:
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
⊢ ↑(⋃ x, (fun x_1 => x_1 * ↑x) ⁻¹' t) ≃ ↑(t * ↑s)
Tactic:
apply Set.BijOn.equiv id
Proof state after:
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
⊢ Set.BijOn id (⋃ x, (fun x_1 => x_1 * ↑x) ⁻¹' t) (t * ↑s)
Theorem: Subgroup.subgroup_mul_card_eq_mul
Proof state before:
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
⊢ Set.BijOn id (⋃ x, (fun x_1 => x_1 * ↑x) ⁻¹' t) (t * ↑s)
Tactic:
convert Set.bijOn_id _
Proof state after:
case h.e'_5
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
⊢ t * ↑s = ⋃ x, (fun x_1 => x_1 * ↑x) ⁻¹' t
Theorem: Subgroup.subgroup_mul_card_eq_mul
Proof state before:
case h.e'_5
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
⊢ t * ↑s = ⋃ x, (fun x_1 => x_1 * ↑x) ⁻¹' t
Tactic:
ext x
Proof state after:
case h.e'_5.h
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
x : α
⊢ x ∈ t * ↑s ↔ x ∈ ⋃ x, (fun x_1 => x_1 * ↑x) ⁻¹' t
Theorem: Subgroup.subgroup_mul_card_eq_mul
Proof state before:
case h.e'_5.h
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
x : α
⊢ x ∈ t * ↑s ↔ x ∈ ⋃ x, (fun x_1 => x_1 * ↑x) ⁻¹' t
Tactic:
constructor
Proof state after:
case h.e'_5.h.mp
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
x : α
⊢ x ∈ t * ↑s → x ∈ ⋃ x, (fun x_1 => x_1 * ↑x) ⁻¹' t

case h.e'_5.h.mpr
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
x : α
⊢ x ∈ ⋃ x, (fun x_1 => x_1 * ↑x) ⁻¹' t → x ∈ t * ↑s
Theorem: Subgroup.subgroup_mul_card_eq_mul
Proof state before:
case h.e'_5.h.mp
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
x : α
⊢ x ∈ t * ↑s → x ∈ ⋃ x, (fun x_1 => x_1 * ↑x) ⁻¹' t
Tactic:
simp only [Set.mem_iUnion, Set.mem_preimage, Subtype.exists, exists_prop, Set.mem_mul]
Proof state after:
case h.e'_5.h.mp
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
x : α
⊢ (∃ x_1 ∈ t, ∃ y ∈ ↑s, x_1 * y = x) → ∃ a ∈ s, x * a ∈ t
Theorem: Subgroup.subgroup_mul_card_eq_mul
Proof state before:
case h.e'_5.h.mp
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
x : α
⊢ (∃ x_1 ∈ t, ∃ y ∈ ↑s, x_1 * y = x) → ∃ a ∈ s, x * a ∈ t
Tactic:
aesop
Proof state after:
no goals
Theorem: Subgroup.subgroup_mul_card_eq_mul
Proof state before:
case h.e'_5.h.mpr
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
x : α
⊢ x ∈ ⋃ x, (fun x_1 => x_1 * ↑x) ⁻¹' t → x ∈ t * ↑s
Tactic:
simp only [Set.mem_iUnion, Set.mem_preimage, Subtype.exists, exists_prop, forall_exists_index,
and_imp]
Proof state after:
case h.e'_5.h.mpr
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
x : α
⊢ ∀ x_1 ∈ s, x * x_1 ∈ t → x ∈ t * ↑s
Theorem: Subgroup.subgroup_mul_card_eq_mul
Proof state before:
case h.e'_5.h.mpr
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
x : α
⊢ ∀ x_1 ∈ s, x * x_1 ∈ t → x ∈ t * ↑s
Tactic:
intro y hys hxy
Proof state after:
case h.e'_5.h.mpr
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
x y : α
hys : y ∈ s
hxy : x * y ∈ t
⊢ x ∈ t * ↑s
Theorem: Subgroup.subgroup_mul_card_eq_mul
Proof state before:
case h.e'_5.h.mpr
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
x y : α
hys : y ∈ s
hxy : x * y ∈ t
⊢ x ∈ t * ↑s
Tactic:
rw [← mul_inv_cancel_right x y]
Proof state after:
case h.e'_5.h.mpr
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
x y : α
hys : y ∈ s
hxy : x * y ∈ t
⊢ x * y * y⁻¹ ∈ t * ↑s
Theorem: Subgroup.subgroup_mul_card_eq_mul
Proof state before:
case h.e'_5.h.mpr
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
x y : α
hys : y ∈ s
hxy : x * y ∈ t
⊢ x * y * y⁻¹ ∈ t * ↑s
Tactic:
apply Set.mul_mem_mul hxy (by simpa)
Proof state after:
no goals
Theorem: Subgroup.subgroup_mul_card_eq_mul
Proof state before:
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a : α
s : Subgroup α
t : Set α
x y : α
hys : y ∈ s
hxy : x * y ∈ t
⊢ y⁻¹ ∈ ↑s
Tactic:
simpa
Proof state after:
no goals
Theorem: Subgroup.pairwiseDisjoint_smul
Proof state before:
α : Type u_1
β : Type u_2
inst✝³ : Group α
inst✝² : Group β
inst✝¹ : MulAction α β
inst✝ : IsScalarTower α β β
s : Subgroup β
⊢ (range fun a => a • ↑s).PairwiseDisjoint id
Tactic:
rintro _ ⟨a, rfl⟩ _ ⟨b, rfl⟩ hab
Proof state after:
case intro.intro
α : Type u_1
β : Type u_2
inst✝³ : Group α
inst✝² : Group β
inst✝¹ : MulAction α β
inst✝ : IsScalarTower α β β
s : Subgroup β
a b : α
hab : (fun a => a • ↑s) a ≠ (fun a => a • ↑s) b
⊢ (Disjoint on id) ((fun a => a • ↑s) a) ((fun a => a • ↑s) b)
Theorem: Subgroup.pairwiseDisjoint_smul
Proof state before:
case intro.intro
α : Type u_1
β : Type u_2
inst✝³ : Group α
inst✝² : Group β
inst✝¹ : MulAction α β
inst✝ : IsScalarTower α β β
s : Subgroup β
a b : α
hab : (fun a => a • ↑s) a ≠ (fun a => a • ↑s) b
⊢ (Disjoint on id) ((fun a => a • ↑s) a) ((fun a => a • ↑s) b)
Tactic:
simp only [Function.onFun, id_eq, disjoint_left] at hab ⊢
Proof state after:
case intro.intro
α : Type u_1
β : Type u_2
inst✝³ : Group α
inst✝² : Group β
inst✝¹ : MulAction α β
inst✝ : IsScalarTower α β β
s : Subgroup β
a b : α
hab : a • ↑s ≠ b • ↑s
⊢ ∀ ⦃a_1 : β⦄, a_1 ∈ a • ↑s → a_1 ∉ b • ↑s
Theorem: Subgroup.pairwiseDisjoint_smul
Proof state before:
case intro.intro
α : Type u_1
β : Type u_2
inst✝³ : Group α
inst✝² : Group β
inst✝¹ : MulAction α β
inst✝ : IsScalarTower α β β
s : Subgroup β
a b : α
hab : a • ↑s ≠ b • ↑s
⊢ ∀ ⦃a_1 : β⦄, a_1 ∈ a • ↑s → a_1 ∉ b • ↑s
Tactic:
rintro _ ⟨c, hc, rfl⟩ ⟨d, hd, (hcd : b • d = a • c)⟩
Proof state after:
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝³ : Group α
inst✝² : Group β
inst✝¹ : MulAction α β
inst✝ : IsScalarTower α β β
s : Subgroup β
a b : α
hab : a • ↑s ≠ b • ↑s
c : β
hc : c ∈ ↑s
d : β
hd : d ∈ ↑s
hcd : b • d = a • c
⊢ False
Theorem: Subgroup.pairwiseDisjoint_smul
Proof state before:
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝³ : Group α
inst✝² : Group β
inst✝¹ : MulAction α β
inst✝ : IsScalarTower α β β
s : Subgroup β
a b : α
hab : a • ↑s ≠ b • ↑s
c : β
hc : c ∈ ↑s
d : β
hd : d ∈ ↑s
hcd : b • d = a • c
⊢ False
Tactic:
refine' hab _
Proof state after:
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝³ : Group α
inst✝² : Group β
inst✝¹ : MulAction α β
inst✝ : IsScalarTower α β β
s : Subgroup β
a b : α
hab : a • ↑s ≠ b • ↑s
c : β
hc : c ∈ ↑s
d : β
hd : d ∈ ↑s
hcd : b • d = a • c
⊢ a • ↑s = b • ↑s
Theorem: Subgroup.pairwiseDisjoint_smul
Proof state before:
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝³ : Group α
inst✝² : Group β
inst✝¹ : MulAction α β
inst✝ : IsScalarTower α β β
s : Subgroup β
a b : α
hab : a • ↑s ≠ b • ↑s
c : β
hc : c ∈ ↑s
d : β
hd : d ∈ ↑s
hcd : b • d = a • c
⊢ a • ↑s = b • ↑s
Tactic:
rw [← smul_coe hc, ← smul_assoc, ← hcd, smul_assoc, smul_coe hc, smul_coe hd]
Proof state after:
no goals
Theorem: Finset.mulImpact_empty
Proof state before:
α : Type u_1
β : Type u_2
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Mul α
n✝ n : ℕ
⊢ ∅.mulImpact n = 0
Tactic:
simp [mulImpact]
Proof state after:
no goals
Theorem: Finset.mulImpact_singleton
Proof state before:
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Group α
n✝ : ℕ
inst✝ : Infinite α
a : α
n : ℕ
⊢ {a}.mulImpact n = n
Tactic:
simp only [mulImpact, singleton_mul', card_smul_finset]
Proof state after:
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Group α
n✝ : ℕ
inst✝ : Infinite α
a : α
n : ℕ
⊢ ⨅ t, (↑t).card = n
Theorem: Finset.mulImpact_singleton
Proof state before:
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Group α
n✝ : ℕ
inst✝ : Infinite α
a : α
n : ℕ
⊢ ⨅ t, (↑t).card = n
Tactic:
haveI : Nonempty {t : Finset α // t.card = n} := nonempty_subtype.2 (exists_card_eq _)
Proof state after:
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Group α
n✝ : ℕ
inst✝ : Infinite α
a : α
n : ℕ
this : Nonempty { t // t.card = n }
⊢ ⨅ t, (↑t).card = n
Theorem: Finset.mulImpact_singleton
Proof state before:
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Group α
n✝ : ℕ
inst✝ : Infinite α
a : α
n : ℕ
this : Nonempty { t // t.card = n }
⊢ ⨅ t, (↑t).card = n
Tactic:
exact Eq.trans (iInf_congr Subtype.prop) ciInf_const
Proof state after:
no goals
Theorem: Finset.mulImpact_map_of_infinite
Proof state before:
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq β
inst✝² : CommGroup α
inst✝¹ : CommGroup β
n : ℕ
inst✝ : Infinite α
s : Finset α
f : α →* β
hf : Injective ⇑f
⊢ (map { toFun := ⇑f, inj' := hf } s).mulImpact n = s.mulImpact n
Tactic:
haveI : Infinite β := sorry
Proof state after:
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq β
inst✝² : CommGroup α
inst✝¹ : CommGroup β
n : ℕ
inst✝ : Infinite α
s : Finset α
f : α →* β
hf : Injective ⇑f
this : Infinite β
⊢ (map { toFun := ⇑f, inj' := hf } s).mulImpact n = s.mulImpact n
Theorem: Finset.mulImpact_map_of_infinite
Proof state before:
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq β
inst✝² : CommGroup α
inst✝¹ : CommGroup β
n : ℕ
inst✝ : Infinite α
s : Finset α
f : α →* β
hf : Injective ⇑f
this : Infinite β
⊢ (map { toFun := ⇑f, inj' := hf } s).mulImpact n = s.mulImpact n
Tactic:
haveI : Nonempty {t : Finset α // t.card = n} := nonempty_subtype.2 (exists_card_eq _)
Proof state after:
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq β
inst✝² : CommGroup α
inst✝¹ : CommGroup β
n : ℕ
inst✝ : Infinite α
s : Finset α
f : α →* β
hf : Injective ⇑f
this✝ : Infinite β
this : Nonempty { t // t.card = n }
⊢ (map { toFun := ⇑f, inj' := hf } s).mulImpact n = s.mulImpact n
Theorem: Finset.mulImpact_map_of_infinite
Proof state before:
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq β
inst✝² : CommGroup α
inst✝¹ : CommGroup β
n : ℕ
inst✝ : Infinite α
s : Finset α
f : α →* β
hf : Injective ⇑f
this✝ : Infinite β
this : Nonempty { t // t.card = n }
⊢ (map { toFun := ⇑f, inj' := hf } s).mulImpact n = s.mulImpact n
Tactic:
haveI : Nonempty {t : Finset β // t.card = n} := nonempty_subtype.2 (exists_card_eq _)
Proof state after:
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq β
inst✝² : CommGroup α
inst✝¹ : CommGroup β
n : ℕ
inst✝ : Infinite α
s : Finset α
f : α →* β
hf : Injective ⇑f
this✝¹ : Infinite β
this✝ : Nonempty { t // t.card = n }
this : Nonempty { t // t.card = n }
⊢ (map { toFun := ⇑f, inj' := hf } s).mulImpact n = s.mulImpact n
Theorem: Finset.mulImpact_map_of_infinite
Proof state before:
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq β
inst✝² : CommGroup α
inst✝¹ : CommGroup β
n : ℕ
inst✝ : Infinite α
s : Finset α
f : α →* β
hf : Injective ⇑f
this✝¹ : Infinite β
this✝ : Nonempty { t // t.card = n }
this : Nonempty { t // t.card = n }
⊢ (map { toFun := ⇑f, inj' := hf } s).mulImpact n = s.mulImpact n
Tactic:
refine' le_antisymm _ _
Proof state after:
case refine'_1
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq β
inst✝² : CommGroup α
inst✝¹ : CommGroup β
n : ℕ
inst✝ : Infinite α
s : Finset α
f : α →* β
hf : Injective ⇑f
this✝¹ : Infinite β
this✝ : Nonempty { t // t.card = n }
this : Nonempty { t // t.card = n }
⊢ (map { toFun := ⇑f, inj' := hf } s).mulImpact n ≤ s.mulImpact n

case refine'_2
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq β
inst✝² : CommGroup α
inst✝¹ : CommGroup β
n : ℕ
inst✝ : Infinite α
s : Finset α
f : α →* β
hf : Injective ⇑f
this✝¹ : Infinite β
this✝ : Nonempty { t // t.card = n }
this : Nonempty { t // t.card = n }
⊢ s.mulImpact n ≤ (map { toFun := ⇑f, inj' := hf } s).mulImpact n