internlm/Lean-Github huggingface dataset:
Theorem: Finset.mulStab_quotient_commute_subgroup
Proof 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
Proof 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
Theorem: Finset.mulStab_quotient_commute_subgroup
Proof 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]
Proof 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
Theorem: Finset.mulStab_quotient_commute_subgroup
Proof 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
Proof 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
Theorem: Finset.mulStab_quotient_commute_subgroup
Proof 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⟩
Proof 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
Theorem: Finset.mulStab_quotient_commute_subgroup
Proof 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)
Proof 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
Theorem: Finset.mulStab_quotient_commute_subgroup
Proof 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]
Proof 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
Theorem: Finset.mulStab_quotient_commute_subgroup
Proof 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, ?_⟩
Proof 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
Theorem: Finset.mulStab_quotient_commute_subgroup
Proof 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]
Proof state after:
no goals
Theorem: Finset.mulStab_quotient_commute_subgroup
Proof 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⟩
Proof 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
Theorem: Finset.mulStab_quotient_commute_subgroup
Proof 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]
Proof 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
Theorem: Finset.mulStab_quotient_commute_subgroup
Proof 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)
Proof 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
Theorem: Finset.mulStab_quotient_commute_subgroup
Proof 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⟩
Proof 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
Theorem: Finset.mulStab_quotient_commute_subgroup
Proof 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]
Proof 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)
Theorem: Finset.mulStab_quotient_commute_subgroup
Proof 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
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
a : α
hax : a ∈ t.mulStab ∧ ↑a = x
z : α ⧸ s
b : α
hbt : b ∈ t
hbz : ↑b = z
⊢ ↑a * ↑(a⁻¹ * b) = ↑b
Tactic:
simp
Proof state after:
no goals
Theorem: Finset.mulStab_quotient_commute_subgroup
Proof 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
Proof 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
Theorem: Finset.mulStab_quotient_commute_subgroup
Proof 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
Proof 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
Theorem: Finset.mulStab_quotient_commute_subgroup
Proof 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
Proof 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
Theorem: Finset.mulStab_quotient_commute_subgroup
Proof 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⟩
Proof 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
Theorem: Finset.mulStab_quotient_commute_subgroup
Proof 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
Proof 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
Theorem: Finset.mulStab_quotient_commute_subgroup
Proof 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)
Proof 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
Theorem: Finset.mulStab_quotient_commute_subgroup
Proof 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
Proof 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
Theorem: Finset.mulStab_quotient_commute_subgroup
Proof 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
Proof 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
Theorem: Finset.mulStab_quotient_commute_subgroup
Proof 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
Proof 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
Theorem: Finset.mulStab_quotient_commute_subgroup
Proof 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
Proof 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
Theorem: Finset.mulStab_quotient_commute_subgroup
Proof 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
Proof 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
Theorem: Finset.mulStab_quotient_commute_subgroup
Proof 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
Proof 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
Theorem: Finset.mulStab_quotient_commute_subgroup
Proof 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
Proof 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
Theorem: Finset.mulStab_quotient_commute_subgroup
Proof 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
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 : (y • b)⁻¹ * z = c
⊢ z ∈ y • t