internlm/Lean-Github huggingface dataset:
Theorem: contains_commutators_of
Proof state before:
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : Subgroup.IsCommutative H
φ : ↥H →* G ⧸ N := MonoidHom.comp (QuotientGroup.mk' N) (Subgroup.subtype H)
S_top : comap (QuotientGroup.mk' N) (MonoidHom.range φ) = ⊤
x : G ⧸ N
a✝ : x ∈ ⊤
y : G := Quotient.out' x
⊢ x ∈ MonoidHom.range φ
Tactic:
have hy : y ∈ φ.range.comap (QuotientGroup.mk' N) := by rw [S_top]; exact Subgroup.mem_top y
Proof state after:
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : Subgroup.IsCommutative H
φ : ↥H →* G ⧸ N := MonoidHom.comp (QuotientGroup.mk' N) (Subgroup.subtype H)
S_top : comap (QuotientGroup.mk' N) (MonoidHom.range φ) = ⊤
x : G ⧸ N
a✝ : x ∈ ⊤
y : G := Quotient.out' x
hy : y ∈ comap (QuotientGroup.mk' N) (MonoidHom.range φ)
⊢ x ∈ MonoidHom.range φ
Theorem: contains_commutators_of
Proof state before:
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : Subgroup.IsCommutative H
φ : ↥H →* G ⧸ N := MonoidHom.comp (QuotientGroup.mk' N) (Subgroup.subtype H)
S_top : comap (QuotientGroup.mk' N) (MonoidHom.range φ) = ⊤
x : G ⧸ N
a✝ : x ∈ ⊤
y : G := Quotient.out' x
hy : y ∈ comap (QuotientGroup.mk' N) (MonoidHom.range φ)
⊢ x ∈ MonoidHom.range φ
Tactic:
rw [← QuotientGroup.out_eq' x]
Proof state after:
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : Subgroup.IsCommutative H
φ : ↥H →* G ⧸ N := MonoidHom.comp (QuotientGroup.mk' N) (Subgroup.subtype H)
S_top : comap (QuotientGroup.mk' N) (MonoidHom.range φ) = ⊤
x : G ⧸ N
a✝ : x ∈ ⊤
y : G := Quotient.out' x
hy : y ∈ comap (QuotientGroup.mk' N) (MonoidHom.range φ)
⊢ ↑(Quotient.out' x) ∈ MonoidHom.range φ
Theorem: contains_commutators_of
Proof state before:
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : Subgroup.IsCommutative H
φ : ↥H →* G ⧸ N := MonoidHom.comp (QuotientGroup.mk' N) (Subgroup.subtype H)
S_top : comap (QuotientGroup.mk' N) (MonoidHom.range φ) = ⊤
x : G ⧸ N
a✝ : x ∈ ⊤
y : G := Quotient.out' x
hy : y ∈ comap (QuotientGroup.mk' N) (MonoidHom.range φ)
⊢ ↑(Quotient.out' x) ∈ MonoidHom.range φ
Tactic:
exact Subgroup.mem_comap.mp hy
Proof state after:
no goals
Theorem: contains_commutators_of
Proof state before:
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : Subgroup.IsCommutative H
φ : ↥H →* G ⧸ N := MonoidHom.comp (QuotientGroup.mk' N) (Subgroup.subtype H)
S_top : comap (QuotientGroup.mk' N) (MonoidHom.range φ) = ⊤
x : G ⧸ N
a✝ : x ∈ ⊤
y : G := Quotient.out' x
⊢ y ∈ comap (QuotientGroup.mk' N) (MonoidHom.range φ)
Tactic:
rw [S_top]
Proof state after:
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : Subgroup.IsCommutative H
φ : ↥H →* G ⧸ N := MonoidHom.comp (QuotientGroup.mk' N) (Subgroup.subtype H)
S_top : comap (QuotientGroup.mk' N) (MonoidHom.range φ) = ⊤
x : G ⧸ N
a✝ : x ∈ ⊤
y : G := Quotient.out' x
⊢ y ∈ ⊤
Theorem: contains_commutators_of
Proof state before:
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : Subgroup.IsCommutative H
φ : ↥H →* G ⧸ N := MonoidHom.comp (QuotientGroup.mk' N) (Subgroup.subtype H)
S_top : comap (QuotientGroup.mk' N) (MonoidHom.range φ) = ⊤
x : G ⧸ N
a✝ : x ∈ ⊤
y : G := Quotient.out' x
⊢ y ∈ ⊤
Tactic:
exact Subgroup.mem_top y
Proof state after:
no goals
Theorem: contains_commutators_of
Proof state before:
case left
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : Subgroup.IsCommutative H
φ : ↥H →* G ⧸ N := MonoidHom.comp (QuotientGroup.mk' N) (Subgroup.subtype H)
⊢ N ≤ comap (QuotientGroup.mk' N) (MonoidHom.range φ)
Tactic:
intro g hg
Proof state after:
case left
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : Subgroup.IsCommutative H
φ : ↥H →* G ⧸ N := MonoidHom.comp (QuotientGroup.mk' N) (Subgroup.subtype H)
g : G
hg : g ∈ N
⊢ g ∈ comap (QuotientGroup.mk' N) (MonoidHom.range φ)
Theorem: contains_commutators_of
Proof state before:
case left
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : Subgroup.IsCommutative H
φ : ↥H →* G ⧸ N := MonoidHom.comp (QuotientGroup.mk' N) (Subgroup.subtype H)
g : G
hg : g ∈ N
⊢ g ∈ comap (QuotientGroup.mk' N) (MonoidHom.range φ)
Tactic:
rw [Subgroup.mem_comap]
Proof state after:
case left
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : Subgroup.IsCommutative H
φ : ↥H →* G ⧸ N := MonoidHom.comp (QuotientGroup.mk' N) (Subgroup.subtype H)
g : G
hg : g ∈ N
⊢ (QuotientGroup.mk' N) g ∈ MonoidHom.range φ
Theorem: contains_commutators_of
Proof state before:
case left
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : Subgroup.IsCommutative H
φ : ↥H →* G ⧸ N := MonoidHom.comp (QuotientGroup.mk' N) (Subgroup.subtype H)
g : G
hg : g ∈ N
⊢ (QuotientGroup.mk' N) g ∈ MonoidHom.range φ
Tactic:
convert (MonoidHom.range φ).one_mem
Proof state after:
case h.e'_4
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : Subgroup.IsCommutative H
φ : ↥H →* G ⧸ N := MonoidHom.comp (QuotientGroup.mk' N) (Subgroup.subtype H)
g : G
hg : g ∈ N
⊢ (QuotientGroup.mk' N) g = 1
Theorem: contains_commutators_of
Proof state before:
case h.e'_4
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : Subgroup.IsCommutative H
φ : ↥H →* G ⧸ N := MonoidHom.comp (QuotientGroup.mk' N) (Subgroup.subtype H)
g : G
hg : g ∈ N
⊢ (QuotientGroup.mk' N) g = 1
Tactic:
simp only [hg, QuotientGroup.mk'_apply, QuotientGroup.eq_one_iff]
Proof state after:
no goals
Theorem: contains_commutators_of
Proof state before:
case right
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : Subgroup.IsCommutative H
φ : ↥H →* G ⧸ N := MonoidHom.comp (QuotientGroup.mk' N) (Subgroup.subtype H)
⊢ H ≤ comap (QuotientGroup.mk' N) (MonoidHom.range φ)
Tactic:
intro h hh
Proof state after:
case right
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : Subgroup.IsCommutative H
φ : ↥H →* G ⧸ N := MonoidHom.comp (QuotientGroup.mk' N) (Subgroup.subtype H)
h : G
hh : h ∈ H
⊢ h ∈ comap (QuotientGroup.mk' N) (MonoidHom.range φ)
Theorem: contains_commutators_of
Proof state before:
case right
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : Subgroup.IsCommutative H
φ : ↥H →* G ⧸ N := MonoidHom.comp (QuotientGroup.mk' N) (Subgroup.subtype H)
h : G
hh : h ∈ H
⊢ h ∈ comap (QuotientGroup.mk' N) (MonoidHom.range φ)
Tactic:
simp only [mem_comap, QuotientGroup.mk'_apply, MonoidHom.mem_range, MonoidHom.coe_comp,
  QuotientGroup.coe_mk', coeSubtype, Function.comp_apply, Subtype.exists, exists_prop, φ]
Proof state after:
case right
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : Subgroup.IsCommutative H
φ : ↥H →* G ⧸ N := MonoidHom.comp (QuotientGroup.mk' N) (Subgroup.subtype H)
h : G
hh : h ∈ H
⊢ ∃ a ∈ H, ↑a = ↑h
Theorem: contains_commutators_of
Proof state before:
case right
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : Normal N
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : Subgroup.IsCommutative H
φ : ↥H →* G ⧸ N := MonoidHom.comp (QuotientGroup.mk' N) (Subgroup.subtype H)
h : G
hh : h ∈ H
⊢ ∃ a ∈ H, ↑a = ↑h
Tactic:
use h
Proof state after:
no goals
Theorem: Equiv.Perm.fixingSubgroup_conj
Proof state before:
α✝ : Type ?u.1776
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
⊢ fixingSubgroup G (g • s) = MulAut.conj g • fixingSubgroup G s
Tactic:
ext k
Proof state after:
case h
α✝ : Type ?u.1776
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g k : G
⊢ k ∈ fixingSubgroup G (g • s) ↔ k ∈ MulAut.conj g • fixingSubgroup G s
Theorem: Equiv.Perm.fixingSubgroup_conj
Proof state before:
case h
α✝ : Type ?u.1776
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g k : G
⊢ k ∈ fixingSubgroup G (g • s) ↔ k ∈ MulAut.conj g • fixingSubgroup G s
Tactic:
simp only [mem_fixingSubgroup_iff, Subgroup.mem_pointwise_smul_iff_inv_smul_mem]
Proof state after:
case h
α✝ : Type ?u.1776
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g k : G
⊢ (∀ y ∈ g • s, k • y = y) ↔ ∀ y ∈ s, ((MulAut.conj g)⁻¹ • k) • y = y
Theorem: Equiv.Perm.fixingSubgroup_conj
Proof state before:
case h
α✝ : Type ?u.1776
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g k : G
⊢ (∀ y ∈ g • s, k • y = y) ↔ ∀ y ∈ s, ((MulAut.conj g)⁻¹ • k) • y = y
Tactic:
rw [Equiv.forall_congr (toPerm g⁻¹)]
Proof state after:
case h
α✝ : Type ?u.1776
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g k : G
⊢ ∀ {x : α}, x ∈ g • s → k • x = x ↔ (toPerm g⁻¹) x ∈ s → ((MulAut.conj g)⁻¹ • k) • (toPerm g⁻¹) x = (toPerm g⁻¹) x
Theorem: Equiv.Perm.fixingSubgroup_conj
Proof state before:
case h
α✝ : Type ?u.1776
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g k : G
⊢ ∀ {x : α}, x ∈ g • s → k • x = x ↔ (toPerm g⁻¹) x ∈ s → ((MulAut.conj g)⁻¹ • k) • (toPerm g⁻¹) x = (toPerm g⁻¹) x
Tactic:
intro x
Proof state after:
case h
α✝ : Type ?u.1776
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g k : G
x : α
⊢ x ∈ g • s → k • x = x ↔ (toPerm g⁻¹) x ∈ s → ((MulAut.conj g)⁻¹ • k) • (toPerm g⁻¹) x = (toPerm g⁻¹) x
Theorem: Equiv.Perm.fixingSubgroup_conj
Proof state before:
case h
α✝ : Type ?u.1776
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g k : G
x : α
⊢ x ∈ g • s → k • x = x ↔ (toPerm g⁻¹) x ∈ s → ((MulAut.conj g)⁻¹ • k) • (toPerm g⁻¹) x = (toPerm g⁻¹) x
Tactic:
simp only [toPerm_apply]
Proof state after:
case h
α✝ : Type ?u.1776
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g k : G
x : α
⊢ x ∈ g • s → k • x = x ↔ g⁻¹ • x ∈ s → ((MulAut.conj g)⁻¹ • k) • g⁻¹ • x = g⁻¹ • x
Theorem: Equiv.Perm.fixingSubgroup_conj
Proof state before:
case h
α✝ : Type ?u.1776
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g k : G
x : α
⊢ x ∈ g • s → k • x = x ↔ g⁻¹ • x ∈ s → ((MulAut.conj g)⁻¹ • k) • g⁻¹ • x = g⁻¹ • x
Tactic:
rw [← Set.mem_smul_set_iff_inv_smul_mem]
Proof state after:
case h
α✝ : Type ?u.1776
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g k : G
x : α
⊢ x ∈ g • s → k • x = x ↔ x ∈ g • s → ((MulAut.conj g)⁻¹ • k) • g⁻¹ • x = g⁻¹ • x
Theorem: Equiv.Perm.fixingSubgroup_conj
Proof state before:
case h
α✝ : Type ?u.1776
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g k : G
x : α
⊢ x ∈ g • s → k • x = x ↔ x ∈ g • s → ((MulAut.conj g)⁻¹ • k) • g⁻¹ • x = g⁻¹ • x
Tactic:
simp only [MulAut.smul_def, MulAut.conj_inv_apply, mul_smul, smul_inv_smul, smul_left_cancel_iff]
Proof state after:
no goals
Theorem: Equiv.Perm.IwasawaT'_isConj
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
⊢ IwasawaT' (g • s) = MulAut.conj g • IwasawaT' s
Tactic:
ext k
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g k : Perm α
⊢ k ∈ IwasawaT' (g • s) ↔ k ∈ MulAut.conj g • IwasawaT' s
Theorem: Equiv.Perm.IwasawaT'_isConj
Proof state before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g k : Perm α
⊢ k ∈ IwasawaT' (g • s) ↔ k ∈ MulAut.conj g • IwasawaT' s
Tactic:
unfold IwasawaT'
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g k : Perm α
⊢ k ∈ fixingSubgroup (Perm α) (↑(g • s))ᶜ ↔ k ∈ MulAut.conj g • fixingSubgroup (Perm α) (↑s)ᶜ
Theorem: Equiv.Perm.IwasawaT'_isConj
Proof state before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g k : Perm α
⊢ k ∈ fixingSubgroup (Perm α) (↑(g • s))ᶜ ↔ k ∈ MulAut.conj g • fixingSubgroup (Perm α) (↑s)ᶜ
Tactic:
simp only [Finset.coe_smul_finset, mem_fixingSubgroup_iff,
  Subgroup.mem_pointwise_smul_iff_inv_smul_mem]
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g k : Perm α
⊢ (∀ y ∈ (g • ↑s)ᶜ, k • y = y) ↔ ∀ y ∈ (↑s)ᶜ, ((MulAut.conj g)⁻¹ • k) • y = y
Theorem: Equiv.Perm.IwasawaT'_isConj
Proof state before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g k : Perm α
⊢ (∀ y ∈ (g • ↑s)ᶜ, k • y = y) ↔ ∀ y ∈ (↑s)ᶜ, ((MulAut.conj g)⁻¹ • k) • y = y
Tactic:
rw [Equiv.forall_congr (toPerm g⁻¹)]
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g k : Perm α
⊢ ∀ {x : α},
    x ∈ (g • ↑s)ᶜ → k • x = x ↔ (toPerm g⁻¹) x ∈ (↑s)ᶜ → ((MulAut.conj g)⁻¹ • k) • (toPerm g⁻¹) x = (toPerm g⁻¹) x
Theorem: Equiv.Perm.IwasawaT'_isConj
Proof state before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g k : Perm α
⊢ ∀ {x : α},
    x ∈ (g • ↑s)ᶜ → k • x = x ↔ (toPerm g⁻¹) x ∈ (↑s)ᶜ → ((MulAut.conj g)⁻¹ • k) • (toPerm g⁻¹) x = (toPerm g⁻¹) x
Tactic:
intro x
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g k : Perm α
x : α
⊢ x ∈ (g • ↑s)ᶜ → k • x = x ↔ (toPerm g⁻¹) x ∈ (↑s)ᶜ → ((MulAut.conj g)⁻¹ • k) • (toPerm g⁻¹) x = (toPerm g⁻¹) x
Theorem: Equiv.Perm.IwasawaT'_isConj
Proof state before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g k : Perm α
x : α
⊢ x ∈ (g • ↑s)ᶜ → k • x = x ↔ (toPerm g⁻¹) x ∈ (↑s)ᶜ → ((MulAut.conj g)⁻¹ • k) • (toPerm g⁻¹) x = (toPerm g⁻¹) x
Tactic:
simp only [toPerm_apply]
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g k : Perm α
x : α
⊢ x ∈ (g • ↑s)ᶜ → k • x = x ↔ g⁻¹ • x ∈ (↑s)ᶜ → ((MulAut.conj g)⁻¹ • k) • g⁻¹ • x = g⁻¹ • x
Theorem: Equiv.Perm.IwasawaT'_isConj
Proof state before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g k : Perm α
x : α
⊢ x ∈ (g • ↑s)ᶜ → k • x = x ↔ g⁻¹ • x ∈ (↑s)ᶜ → ((MulAut.conj g)⁻¹ • k) • g⁻¹ • x = g⁻¹ • x
Tactic:
rw [← Set.mem_smul_set_iff_inv_smul_mem]
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g k : Perm α
x : α
⊢ x ∈ (g • ↑s)ᶜ → k • x = x ↔ x ∈ g • (↑s)ᶜ → ((MulAut.conj g)⁻¹ • k) • g⁻¹ • x = g⁻¹ • x
Theorem: Equiv.Perm.IwasawaT'_isConj
Proof state before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g k : Perm α
x : α
⊢ x ∈ (g • ↑s)ᶜ → k • x = x ↔ x ∈ g • (↑s)ᶜ → ((MulAut.conj g)⁻¹ • k) • g⁻¹ • x = g⁻¹ • x
Tactic:
simp only [Set.mem_compl_iff, Perm.smul_def, smul_compl_set, MulAut.smul_def,
  MulAut.conj_inv_apply, coe_mul, Function.comp_apply, apply_inv_self,
  EmbeddingLike.apply_eq_iff_eq]
Proof state after:
no goals
Theorem: Equiv.Perm.Equiv.Perm.ofSubtype_range_eq
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
⊢ MonoidHom.range ofSubtype = fixingSubgroup (Perm α) sᶜ
Tactic:
ext k
Proof state after:
case h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
⊢ k ∈ MonoidHom.range ofSubtype ↔ k ∈ fixingSubgroup (Perm α) sᶜ
Theorem: Equiv.Perm.Equiv.Perm.ofSubtype_range_eq
Proof state before:
case h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
⊢ k ∈ MonoidHom.range ofSubtype ↔ k ∈ fixingSubgroup (Perm α) sᶜ
Tactic:
simp only [mem_fixingSubgroup_iff, Set.mem_compl_iff, Finset.mem_coe, Perm.smul_def, Finset.coe_sort_coe,
  MonoidHom.mem_range]
Proof state after:
case h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
⊢ (∃ x, ofSubtype x = k) ↔ ∀ y ∉ s, k y = y
Theorem: Equiv.Perm.Equiv.Perm.ofSubtype_range_eq
Proof state before:
case h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
⊢ (∃ x, ofSubtype x = k) ↔ ∀ y ∉ s, k y = y
Tactic:
constructor
Proof state after:
case h.mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
⊢ (∃ x, ofSubtype x = k) → ∀ y ∉ s, k y = y

case h.mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
⊢ (∀ y ∉ s, k y = y) → ∃ x, ofSubtype x = k
Theorem: Equiv.Perm.Equiv.Perm.ofSubtype_range_eq
Proof state before:
case h.mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
⊢ (∃ x, ofSubtype x = k) → ∀ y ∉ s, k y = y
Tactic:
rintro ⟨k, rfl⟩
Proof state after:
case h.mp.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm { x // x ∈ s }
⊢ ∀ y ∉ s, (ofSubtype k) y = y
Theorem: Equiv.Perm.Equiv.Perm.ofSubtype_range_eq
Proof state before:
case h.mp.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm { x // x ∈ s }
⊢ ∀ y ∉ s, (ofSubtype k) y = y
Tactic:
intro y hy
Proof state after:
case h.mp.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm { x // x ∈ s }
y : α
hy : y ∉ s
⊢ (ofSubtype k) y = y
Theorem: Equiv.Perm.Equiv.Perm.ofSubtype_range_eq
Proof state before:
case h.mp.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm { x // x ∈ s }
y : α
hy : y ∉ s
⊢ (ofSubtype k) y = y
Tactic:
rw [ofSubtype_apply_of_not_mem k hy]
Proof state after:
no goals
Theorem: Equiv.Perm.Equiv.Perm.ofSubtype_range_eq
Proof state before:
case h.mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
⊢ (∀ y ∉ s, k y = y) → ∃ x, ofSubtype x = k
Tactic:
intro h
Proof state after:
case h.mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
⊢ ∃ x, ofSubtype x = k
Theorem: Equiv.Perm.Equiv.Perm.ofSubtype_range_eq
Proof state before:
case h.mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
hks : s = k • s
⊢ ∃ x, ofSubtype x = k
Tactic:
suffices hk' : _ by
  use Equiv.Perm.subtypePerm k hk'
  rw [Equiv.Perm.ofSubtype_subtypePerm]
  simp only [ne_eq, Finset.mem_coe]
  intro x
  rw [not_imp_comm]
  exact h x
Proof state after:
case h.mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
hks : s = k • s
⊢ ∀ (x : α), x ∈ s ↔ k x ∈ s
Theorem: Equiv.Perm.Equiv.Perm.ofSubtype_range_eq
Proof state before:
case h.mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
hks : s = k • s
⊢ ∀ (x : α), x ∈ s ↔ k x ∈ s
Tactic:
intro x
Proof state after:
case h.mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
hks : s = k • s
x : α
⊢ x ∈ s ↔ k x ∈ s
Theorem: Equiv.Perm.Equiv.Perm.ofSubtype_range_eq
Proof state before:
case h.mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
hks : s = k • s
x : α
⊢ x ∈ s ↔ k x ∈ s
Tactic:
rw [← Equiv.Perm.smul_def]
Proof state after:
case h.mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
hks : s = k • s
x : α
⊢ x ∈ s ↔ k • x ∈ s
Theorem: Equiv.Perm.Equiv.Perm.ofSubtype_range_eq
Proof state before:
case h.mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
hks : s = k • s
x : α
⊢ x ∈ s ↔ k • x ∈ s
Tactic:
nth_rewrite 2 [hks]
Proof state after:
case h.mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
hks : s = k • s
x : α
⊢ x ∈ s ↔ k • x ∈ k • s
Theorem: Equiv.Perm.Equiv.Perm.ofSubtype_range_eq
Proof state before:
case h.mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
hks : s = k • s
x : α
⊢ x ∈ s ↔ k • x ∈ k • s
Tactic:
rw [Set.smul_mem_smul_set_iff]
Proof state after:
no goals
Theorem: Equiv.Perm.Equiv.Perm.ofSubtype_range_eq
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
⊢ s = k • s
Tactic:
apply le_antisymm
Proof state after:
case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
⊢ s ≤ k • s

case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
⊢ k • s ≤ s
Theorem: Equiv.Perm.Equiv.Perm.ofSubtype_range_eq
Proof state before:
case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
⊢ s ≤ k • s

case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
⊢ k • s ≤ s
Tactic:
. intro x hx
  rw [Set.mem_smul_set_iff_inv_smul_mem, Perm.smul_def]
  by_contra hx'
  rw [← h _ hx', apply_inv_self] at hx'
  exact hx' hx
Proof state after:
case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
⊢ k • s ≤ s
Theorem: Equiv.Perm.Equiv.Perm.ofSubtype_range_eq
Proof state before:
case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
⊢ s ≤ k • s
Tactic:
intro x hx
Proof state after:
case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
x : α
hx : x ∈ s
⊢ x ∈ k • s
Theorem: Equiv.Perm.Equiv.Perm.ofSubtype_range_eq
Proof state before:
case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
x : α
hx : x ∈ s
⊢ x ∈ k • s
Tactic:
rw [Set.mem_smul_set_iff_inv_smul_mem, Perm.smul_def]
Proof state after:
case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
x : α
hx : x ∈ s
⊢ k⁻¹ x ∈ s
Theorem: Equiv.Perm.Equiv.Perm.ofSubtype_range_eq
Proof state before:
case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
x : α
hx : x ∈ s
⊢ k⁻¹ x ∈ s
Tactic:
by_contra hx'
Proof state after:
case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
x : α
hx : x ∈ s
hx' : k⁻¹ x ∉ s
⊢ False
Theorem: Equiv.Perm.Equiv.Perm.ofSubtype_range_eq
Proof state before:
case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
x : α
hx : x ∈ s
hx' : k⁻¹ x ∉ s
⊢ False
Tactic:
rw [← h _ hx', apply_inv_self] at hx'
Proof state after:
case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
x : α
hx : x ∈ s
hx' : x ∉ s
⊢ False