Theorem: Finset.mulStab_quotient_commute_subgroup (LeanCamCombi/Kneser/MulStab.lean)

State before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
⊢ image QuotientGroup.mk t.mulStab = (image QuotientGroup.mk t).mulStab
Tactic:
obtain rfl | ht := t.eq_empty_or_nonempty
State after:
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
a : α
s : Subgroup α
hst : ↑s ⊆ ↑∅.mulStab
⊢ image QuotientGroup.mk ∅.mulStab = (image QuotientGroup.mk ∅).mulStab

case inr
ι : 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
⊢ image QuotientGroup.mk t.mulStab = (image QuotientGroup.mk t).mulStab

State before:
case inr
ι : 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
⊢ image QuotientGroup.mk t.mulStab = (image QuotientGroup.mk t).mulStab
Tactic:
have hti : (image (QuotientGroup.mk (s := s)) t).Nonempty := by aesop
State after:
case inr
ι : 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
⊢ image QuotientGroup.mk t.mulStab = (image QuotientGroup.mk t).mulStab

State before:
case inr
ι : 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
⊢ image QuotientGroup.mk t.mulStab = (image QuotientGroup.mk t).mulStab
Tactic:
ext x
State after:
case inr.a
ι : 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
⊢ x ∈ image QuotientGroup.mk t.mulStab ↔ x ∈ (image QuotientGroup.mk t).mulStab

State before:
case inr.a
ι : 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
⊢ x ∈ image QuotientGroup.mk t.mulStab ↔ x ∈ (image QuotientGroup.mk t).mulStab
Tactic:
simp only [mem_image, image_nonempty, mem_mulStab hti]
State after:
case inr.a
ι : 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
⊢ (∃ a ∈ t.mulStab, ↑a = x) ↔ x • image QuotientGroup.mk t = image QuotientGroup.mk t

State before:
case inr.a
ι : 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
⊢ (∃ a ∈ t.mulStab, ↑a = x) ↔ x • image QuotientGroup.mk t = image QuotientGroup.mk t
Tactic:
constructor
State after:
case inr.a.mp
ι : 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
⊢ (∃ a ∈ t.mulStab, ↑a = x) → x • image QuotientGroup.mk t = image QuotientGroup.mk t

case inr.a.mpr
ι : 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
⊢ x • image QuotientGroup.mk t = image QuotientGroup.mk t → ∃ a ∈ t.mulStab, ↑a = x

State before:
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
a : α
s : Subgroup α
hst : ↑s ⊆ ↑∅.mulStab
⊢ image QuotientGroup.mk ∅.mulStab = (image QuotientGroup.mk ∅).mulStab
Tactic:
simp
State after:
no goals

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
⊢ (image QuotientGroup.mk t).Nonempty
Tactic:
aesop
State after:
no goals

State before:
case inr.a.mp
ι : 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
⊢ (∃ a ∈ t.mulStab, ↑a = x) → x • image QuotientGroup.mk t = image QuotientGroup.mk t
Tactic:
rintro ⟨a, hax⟩
State after:
case inr.a.mp.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
a : α
hax : a ∈ t.mulStab ∧ ↑a = x
⊢ x • image QuotientGroup.mk t = image QuotientGroup.mk t

State before:
case inr.a.mp.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
a : α
hax : a ∈ t.mulStab ∧ ↑a = x
⊢ x • image QuotientGroup.mk t = image QuotientGroup.mk t
Tactic:
rw [← hax.2]
State after:
case inr.a.mp.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
a : α
hax : a ∈ t.mulStab ∧ ↑a = x
⊢ ↑a • image QuotientGroup.mk t = image QuotientGroup.mk t

State before:
case inr.a.mp.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
a : α
hax : a ∈ t.mulStab ∧ ↑a = x
⊢ ↑a • image QuotientGroup.mk t = image QuotientGroup.mk t
Tactic:
ext z
State after:
case inr.a.mp.intro.a
ι : 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
a : α
hax : a ∈ t.mulStab ∧ ↑a = x
z : α ⧸ s
⊢ z ∈ ↑a • image QuotientGroup.mk t ↔ z ∈ image QuotientGroup.mk t

State before:
case inr.a.mp.intro.a
ι : 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
a : α
hax : a ∈ t.mulStab ∧ ↑a = x
z : α ⧸ s
⊢ z ∈ ↑a • image QuotientGroup.mk t ↔ z ∈ image QuotientGroup.mk t
Tactic:
simp only [mem_smul_finset, mem_image, smul_eq_mul, exists_exists_and_eq_and]
State after:
case inr.a.mp.intro.a
ι : 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
a : α
hax : a ∈ t.mulStab ∧ ↑a = x
z : α ⧸ s
⊢ (∃ a_1 ∈ t, ↑a * ↑a_1 = z) ↔ ∃ a ∈ t, ↑a = z

State before:
case inr.a.mp.intro.a
ι : 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
a : α
hax : a ∈ t.mulStab ∧ ↑a = x
z : α ⧸ s
⊢ (∃ a_1 ∈ t, ↑a * ↑a_1 = z) ↔ ∃ a ∈ t, ↑a = z
Tactic:
constructor
State after:
case inr.a.mp.intro.a.mp
ι : 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
a : α
hax : a ∈ t.mulStab ∧ ↑a = x
z : α ⧸ s
⊢ (∃ a_1 ∈ t, ↑a * ↑a_1 = z) → ∃ a ∈ t, ↑a = z

case inr.a.mp.intro.a.mpr
ι : 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
a : α
hax : a ∈ t.mulStab ∧ ↑a = x
z : α ⧸ s
⊢ (∃ a ∈ t, ↑a = z) → ∃ a_2 ∈ t, ↑a * ↑a_2 = z

State before:
case inr.a.mp.intro.a.mp
ι : 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
a : α
hax : a ∈ t.mulStab ∧ ↑a = x
z : α ⧸ s
⊢ (∃ a_1 ∈ t, ↑a * ↑a_1 = z) → ∃ a ∈ t, ↑a = z
Tactic:
rintro ⟨b, hbt, hbaz⟩
State after:
case inr.a.mp.intro.a.mp.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
a : α
hax : a ∈ t.mulStab ∧ ↑a = x
z : α ⧸ s
b : α
hbt : b ∈ t
hbaz : ↑a * ↑b = z
⊢ ∃ a ∈ t, ↑a = z

State before:
case inr.a.mp.intro.a.mp.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
a : α
hax : a ∈ t.mulStab ∧ ↑a = x
z : α ⧸ s
b : α
hbt : b ∈ t
hbaz : ↑a * ↑b = z
⊢ ∃ a ∈ t, ↑a = z
Tactic:
use (b * a)
State after:
case h
ι : 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
a : α
hax : a ∈ t.mulStab ∧ ↑a = x
z : α ⧸ s
b : α
hbt : b ∈ t
hbaz : ↑a * ↑b = z
⊢ b * a ∈ t ∧ ↑(b * a) = z

State before:
case h
ι : 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
a : α
hax : a ∈ t.mulStab ∧ ↑a = x
z : α ⧸ s
b : α
hbt : b ∈ t
hbaz : ↑a * ↑b = z
⊢ b * a ∈ t ∧ ↑(b * a) = z
Tactic:
rw [← mul_mulStab t]
State after:
case h
ι : 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
a : α
hax : a ∈ t.mulStab ∧ ↑a = x
z : α ⧸ s
b : α
hbt : b ∈ t
hbaz : ↑a * ↑b = z
⊢ b * a ∈ t * t.mulStab ∧ ↑(b * a) = z

State before:
case h
ι : 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
a : α
hax : a ∈ t.mulStab ∧ ↑a = x
z : α ⧸ s
b : α
hbt : b ∈ t
hbaz : ↑a * ↑b = z
⊢ b * a ∈ t * t.mulStab ∧ ↑(b * a) = z
Tactic:
refine ⟨mul_mem_mul hbt hax.1, ?_⟩
State after:
case h
ι : 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
a : α
hax : a ∈ t.mulStab ∧ ↑a = x
z : α ⧸ s
b : α
hbt : b ∈ t
hbaz : ↑a * ↑b = z
⊢ ↑(b * a) = z

State before:
case h
ι : 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
a : α
hax : a ∈ t.mulStab ∧ ↑a = x
z : α ⧸ s
b : α
hbt : b ∈ t
hbaz : ↑a * ↑b = z
⊢ ↑(b * a) = z
Tactic:
rw [← hbaz, QuotientGroup.mk_mul, mul_comm]
State after:
no goals

State before:
case inr.a.mp.intro.a.mpr
ι : 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
a : α
hax : a ∈ t.mulStab ∧ ↑a = x
z : α ⧸ s
⊢ (∃ a ∈ t, ↑a = z) → ∃ a_2 ∈ t, ↑a * ↑a_2 = z
Tactic:
rintro ⟨b, hbt, hbz⟩
State after:
case inr.a.mp.intro.a.mpr.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
a : α
hax : a ∈ t.mulStab ∧ ↑a = x
z : α ⧸ s
b : α
hbt : b ∈ t
hbz : ↑b = z
⊢ ∃ a_1 ∈ t, ↑a * ↑a_1 = z

State before:
case inr.a.mp.intro.a.mpr.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
a : α
hax : a ∈ t.mulStab ∧ ↑a = x
z : α ⧸ s
b : α
hbt : b ∈ t
hbz : ↑b = z
⊢ ∃ a_1 ∈ t, ↑a * ↑a_1 = z
Tactic:
rw [← hbz, ← mul_mulStab t, mul_comm]
State after:
case inr.a.mp.intro.a.mpr.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
a : α
hax : a ∈ t.mulStab ∧ ↑a = x
z : α ⧸ s
b : α
hbt : b ∈ t
hbz : ↑b = z
⊢ ∃ a_1 ∈ t.mulStab * t, ↑a * ↑a_1 = ↑b

State before:
case inr.a.mp.intro.a.mpr.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
a : α
hax : a ∈ t.mulStab ∧ ↑a = x
z : α ⧸ s
b : α
hbt : b ∈ t
hbz : ↑b = z
⊢ ∃ a_1 ∈ t.mulStab * t, ↑a * ↑a_1 = ↑b
Tactic:
use (a⁻¹ * b)
State after:
case h
ι : 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
a : α
hax : a ∈ t.mulStab ∧ ↑a = x
z : α ⧸ s
b : α
hbt : b ∈ t
hbz : ↑b = z
⊢ a⁻¹ * b ∈ t.mulStab * t ∧ ↑a * ↑(a⁻¹ * b) = ↑b

State before:
case h
ι : 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
a : α
hax : a ∈ t.mulStab ∧ ↑a = x
z : α ⧸ s
b : α
hbt : b ∈ t
hbz : ↑b = z
⊢ a⁻¹ * b ∈ t.mulStab * t ∧ ↑a * ↑(a⁻¹ * b) = ↑b
Tactic:
refine ⟨mul_mem_mul ?_ hbt, by simp⟩
State after:
case h
ι : 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
a : α
hax : a ∈ t.mulStab ∧ ↑a = x
z : α ⧸ s
b : α
hbt : b ∈ t
hbz : ↑b = z
⊢ a⁻¹ ∈ t.mulStab

State before:
case h
ι : 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
a : α
hax : a ∈ t.mulStab ∧ ↑a = x
z : α ⧸ s
b : α
hbt : b ∈ t
hbz : ↑b = z
⊢ a⁻¹ ∈ t.mulStab
Tactic:
rw [← mem_coe, coe_mulStab ht]
State after:
case h
ι : 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
a : α
hax : a ∈ t.mulStab ∧ ↑a = x
z : α ⧸ s
b : α
hbt : b ∈ t
hbz : ↑b = z
⊢ a⁻¹ ∈ ↑(stabilizer α t)

State before:
case h
ι : 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
a : α
hax : a ∈ t.mulStab ∧ ↑a = x
z : α ⧸ s
b : α
hbt : b ∈ t
hbz : ↑b = z
⊢ a⁻¹ ∈ ↑(stabilizer α t)
Tactic:
aesop
State after:
no goals

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
a : α
hax : a ∈ t.mulStab ∧ ↑a = x
z : α ⧸ s
b : α
hbt : b ∈ t
hbz : ↑b = z
⊢ ↑a * ↑(a⁻¹ * b) = ↑b
Tactic:
simp
State after:
no goals

State before:
case inr.a.mpr
ι : 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
⊢ x • image QuotientGroup.mk t = image QuotientGroup.mk t → ∃ a ∈ t.mulStab, ↑a = x
Tactic:
intro hx
State after:
case inr.a.mpr
ι : 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
⊢ ∃ a ∈ t.mulStab, ↑a = x

State before:
case inr.a.mpr
ι : 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
⊢ ∃ a ∈ t.mulStab, ↑a = x
Tactic:
have : s ≤ stabilizer α t := by aesop
State after:
case inr.a.mpr
ι : 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
⊢ ∃ a ∈ t.mulStab, ↑a = x

State before:
case inr.a.mpr
ι : 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
⊢ ∃ a ∈ t.mulStab, ↑a = x
Tactic:
obtain ⟨y, hyx⟩ := Quotient.exists_rep x
State after:
case inr.a.mpr.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
hx : x • image QuotientGroup.mk t = image QuotientGroup.mk t
this : s ≤ stabilizer α t
y : α
hyx : ⟦y⟧ = x
⊢ ∃ a ∈ t.mulStab, ↑a = x

State before:
case inr.a.mpr.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
hx : x • image QuotientGroup.mk t = image QuotientGroup.mk t
this : s ≤ stabilizer α t
y : α
hyx : ⟦y⟧ = x
⊢ ∃ a ∈ t.mulStab, ↑a = x
Tactic:
refine ⟨y, (mem_mulStab_iff_subset_smul_finset ht).mpr ?_, by simpa⟩
State after:
case inr.a.mpr.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
hx : x • image QuotientGroup.mk t = image QuotientGroup.mk t
this : s ≤ stabilizer α t
y : α
hyx : ⟦y⟧ = x
⊢ t ⊆ y • t

State before:
case inr.a.mpr.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
hx : x • image QuotientGroup.mk t = image QuotientGroup.mk t
this : s ≤ stabilizer α t
y : α
hyx : ⟦y⟧ = x
⊢ t ⊆ y • t
Tactic:
intros z hzt
State after:
case inr.a.mpr.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
hx : x • image QuotientGroup.mk t = image QuotientGroup.mk t
this : s ≤ stabilizer α t
y : α
hyx : ⟦y⟧ = x
z : α
hzt : z ∈ t
⊢ z ∈ y • t

State before:
case inr.a.mpr.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
hx : x • image QuotientGroup.mk t = image QuotientGroup.mk t
this : s ≤ stabilizer α t
y : α
hyx : ⟦y⟧ = x
z : α
hzt : z ∈ t
⊢ z ∈ y • t
Tactic:
replace hx : image QuotientGroup.mk (y • t) = image (QuotientGroup.mk (s := s)) t := by
  rw [← hx, ← hyx]
  exact image_smul_comm QuotientGroup.mk y t (congrFun rfl)
State after:
case inr.a.mpr.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
this : s ≤ stabilizer α t
y : α
hyx : ⟦y⟧ = x
z : α
hzt : z ∈ t
hx : image QuotientGroup.mk (y • t) = image QuotientGroup.mk t
⊢ z ∈ y • t

State before:
case inr.a.mpr.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
this : s ≤ stabilizer α t
y : α
hyx : ⟦y⟧ = x
z : α
hzt : z ∈ t
hx : image QuotientGroup.mk (y • t) = image QuotientGroup.mk t
⊢ z ∈ y • t
Tactic:
have hyz : QuotientGroup.mk z ∈ image (QuotientGroup.mk (s := s)) (y • t) := by aesop
State after:
case inr.a.mpr.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
this : s ≤ stabilizer α t
y : α
hyx : ⟦y⟧ = x
z : α
hzt : z ∈ t
hx : image QuotientGroup.mk (y • t) = image QuotientGroup.mk t
hyz : ↑z ∈ image QuotientGroup.mk (y • t)
⊢ z ∈ y • t

State before:
case inr.a.mpr.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
this : s ≤ stabilizer α t
y : α
hyx : ⟦y⟧ = x
z : α
hzt : z ∈ t
hx : image QuotientGroup.mk (y • t) = image QuotientGroup.mk t
hyz : ↑z ∈ image QuotientGroup.mk (y • t)
⊢ z ∈ y • t
Tactic:
simp only [QuotientGroup.mk_mul, mem_image] at hyz
State after:
case inr.a.mpr.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
this : s ≤ stabilizer α t
y : α
hyx : ⟦y⟧ = x
z : α
hzt : z ∈ t
hx : image QuotientGroup.mk (y • t) = image QuotientGroup.mk t
hyz : ∃ a ∈ y • t, ↑a = ↑z
⊢ z ∈ y • t

State before:
case inr.a.mpr.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
this : s ≤ stabilizer α t
y : α
hyx : ⟦y⟧ = x
z : α
hzt : z ∈ t
hx : image QuotientGroup.mk (y • t) = image QuotientGroup.mk t
hyz : ∃ a ∈ y • t, ↑a = ↑z
⊢ z ∈ y • t
Tactic:
obtain ⟨a, ha, hayz⟩ := hyz
State after:
case inr.a.mpr.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
this : s ≤ stabilizer α t
y : α
hyx : ⟦y⟧ = x
z : α
hzt : z ∈ t
hx : image QuotientGroup.mk (y • t) = image QuotientGroup.mk t
a : α
ha : a ∈ y • t
hayz : ↑a = ↑z
⊢ z ∈ y • t

State before:
case inr.a.mpr.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
this : s ≤ stabilizer α t
y : α
hyx : ⟦y⟧ = x
z : α
hzt : z ∈ t
hx : image QuotientGroup.mk (y • t) = image QuotientGroup.mk t
a : α
ha : a ∈ y • t
hayz : ↑a = ↑z
⊢ z ∈ y • t
Tactic:
obtain ⟨b, hbt, haby⟩ := mem_smul_finset.mp ha
State after:
case inr.a.mpr.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
this : s ≤ stabilizer α t
y : α
hyx : ⟦y⟧ = x
z : α
hzt : z ∈ t
hx : image QuotientGroup.mk (y • t) = image QuotientGroup.mk t
a : α
ha : a ∈ y • t
hayz : ↑a = ↑z
b : α
hbt : b ∈ t
haby : y • b = a
⊢ z ∈ y • t

State before:
case inr.a.mpr.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
this : s ≤ stabilizer α t
y : α
hyx : ⟦y⟧ = x
z : α
hzt : z ∈ t
hx : image QuotientGroup.mk (y • t) = image QuotientGroup.mk t
a : α
ha : a ∈ y • t
hayz : ↑a = ↑z
b : α
hbt : b ∈ t
haby : y • b = a
⊢ z ∈ y • t
Tactic:
subst a
State after:
case inr.a.mpr.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
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
⊢ z ∈ y • t

State before:
case inr.a.mpr.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
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
⊢ z ∈ y • t
Tactic:
rw [QuotientGroup.eq, smul_eq_mul] at hayz
State after:
case inr.a.mpr.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
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
⊢ z ∈ y • t

State before:
case inr.a.mpr.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
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
⊢ z ∈ y • t
Tactic:
replace : ∃ c ∈ mulStab t, (y • b)⁻¹ * z = c := by aesop
State after:
case inr.a.mpr.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
this : ∃ c ∈ t.mulStab, (y • b)⁻¹ * z = c
⊢ z ∈ y • t

State before:
case inr.a.mpr.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
this : ∃ c ∈ t.mulStab, (y • b)⁻¹ * z = c
⊢ z ∈ y • t
Tactic:
obtain ⟨c, hct, hcbyz⟩ := this
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 : (y • b)⁻¹ * z = c
⊢ z ∈ y • t

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
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

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]
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

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)
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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]
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

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)
State after:
no goals

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
State after:
no goals

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
State after:
no goals