internlm/Lean-Github huggingface dataset:
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' : x ∉ s
⊢ False
Tactic:
exact hx' hx
Proof state after:
no goals
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
⊢ k • s ≤ s
Tactic:
intro a ha
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
a : α
ha : a ∈ k • s
⊢ a ∈ 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
a : α
ha : a ∈ k • s
⊢ a ∈ s
Tactic:
by_contra ha'
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
a : α
ha : a ∈ k • s
ha' : a ∉ 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
a : α
ha : a ∈ k • s
ha' : a ∉ s
⊢ False
Tactic:
rw [← h _ ha', ← Perm.smul_def, Set.smul_mem_smul_set_iff] at ha
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
a : α
ha : a ∈ s
ha' : a ∉ 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
a : α
ha : a ∈ s
ha' : a ∉ s
⊢ False
Tactic:
exact ha' ha
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
hks : s = k • s
hk' : ?m.15812
⊢ ∃ x, ofSubtype x = k
Tactic:
use Equiv.Perm.subtypePerm k hk'
Proof state after:
case h
α : 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
hk' : ∀ (x : α), x ∈ s ↔ k x ∈ s
⊢ ofSubtype (subtypePerm k hk') = k
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 α
h : ∀ y ∉ s, k y = y
hks : s = k • s
hk' : ∀ (x : α), x ∈ s ↔ k x ∈ s
⊢ ofSubtype (subtypePerm k hk') = k
Tactic:
rw [Equiv.Perm.ofSubtype_subtypePerm]
Proof state after:
case h.h₂
α : 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
hk' : ∀ (x : α), x ∈ s ↔ k x ∈ s
⊢ ∀ (x : α), k x ≠ x → x ∈ s
Theorem: Equiv.Perm.Equiv.Perm.ofSubtype_range_eq
Proof state before:
case h.h₂
α : 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
hk' : ∀ (x : α), x ∈ s ↔ k x ∈ s
⊢ ∀ (x : α), k x ≠ x → x ∈ s
Tactic:
simp only [ne_eq, Finset.mem_coe]
Proof state after:
case h.h₂
α : 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
hk' : ∀ (x : α), x ∈ s ↔ k x ∈ s
⊢ ∀ (x : α), ¬k x = x → x ∈ s
Theorem: Equiv.Perm.Equiv.Perm.ofSubtype_range_eq
Proof state before:
case h.h₂
α : 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
hk' : ∀ (x : α), x ∈ s ↔ k x ∈ s
⊢ ∀ (x : α), ¬k x = x → x ∈ s
Tactic:
intro x
Proof state after:
case h.h₂
α : 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
hk' : ∀ (x : α), x ∈ s ↔ k x ∈ s
x : α
⊢ ¬k x = x → x ∈ s
Theorem: Equiv.Perm.Equiv.Perm.ofSubtype_range_eq
Proof state before:
case h.h₂
α : 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
hk' : ∀ (x : α), x ∈ s ↔ k x ∈ s
x : α
⊢ ¬k x = x → x ∈ s
Tactic:
rw [not_imp_comm]
Proof state after:
case h.h₂
α : 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
hk' : ∀ (x : α), x ∈ s ↔ k x ∈ s
x : α
⊢ x ∉ s → k x = x
Theorem: Equiv.Perm.Equiv.Perm.ofSubtype_range_eq
Proof state before:
case h.h₂
α : 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
hk' : ∀ (x : α), x ∈ s ↔ k x ∈ s
x : α
⊢ x ∉ s → k x = x
Tactic:
exact h x
Proof state after:
no goals
Theorem: MulAction.smul_compl_set_eq
Proof state before:
α✝ : Type ?u.17129
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
⊢ (g • s)ᶜ = g • sᶜ
Tactic:
ext k
Proof state after:
case h
α✝ : Type ?u.17129
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
k : α
⊢ k ∈ (g • s)ᶜ ↔ k ∈ g • sᶜ
Theorem: MulAction.smul_compl_set_eq
Proof state before:
case h
α✝ : Type ?u.17129
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
k : α
⊢ k ∈ (g • s)ᶜ ↔ k ∈ g • sᶜ
Tactic:
simp only [Set.mem_compl_iff, smul_compl_set]
Proof state after:
no goals
Theorem: Equiv.Perm.this1
Proof state before:
α : Type ?u.19573
inst✝³ : DecidableEq α
inst✝² : Fintype α
G : Type u_1
H : Type u_2
inst✝¹ : Group H
inst✝ : Group G
f : H →* G
g : G
⊢ MulAut.conj g • MonoidHom.range f = MonoidHom.range (MonoidHom.comp (MulEquiv.toMonoidHom (MulAut.conj g)) f)
Tactic:
simp only [← MonoidHom.map_range]
Proof state after:
α : Type ?u.19573
inst✝³ : DecidableEq α
inst✝² : Fintype α
G : Type u_1
H : Type u_2
inst✝¹ : Group H
inst✝ : Group G
f : H →* G
g : G
⊢ MulAut.conj g • MonoidHom.range f = Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) (MonoidHom.range f)
Theorem: Equiv.Perm.this1
Proof state before:
α : Type ?u.19573
inst✝³ : DecidableEq α
inst✝² : Fintype α
G : Type u_1
H : Type u_2
inst✝¹ : Group H
inst✝ : Group G
f : H →* G
g : G
⊢ MulAut.conj g • MonoidHom.range f = Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) (MonoidHom.range f)
Tactic:
rfl
Proof state after:
no goals
Theorem: Equiv.Perm.IwasawaT_is_conj'
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
⊢ IwasawaT (g • s) = MulAut.conj g • IwasawaT s
Tactic:
unfold IwasawaT
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
⊢ MonoidHom.range (Iwt (g • s)) = MulAut.conj g • MonoidHom.range (Iwt s)
Theorem: Equiv.Perm.IwasawaT_is_conj'
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
⊢ MonoidHom.range (Iwt (g • s)) = MulAut.conj g • MonoidHom.range (Iwt s)
Tactic:
unfold Iwt
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
⊢ MonoidHom.range ofSubtype = MulAut.conj g • MonoidHom.range ofSubtype
Theorem: Equiv.Perm.IwasawaT_is_conj'
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
⊢ MonoidHom.range ofSubtype = MulAut.conj g • MonoidHom.range ofSubtype
Tactic:
simp only [Equiv.Perm.ofSubtype_range_eq]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
⊢ fixingSubgroup (Perm α) (↑(g • s))ᶜ = MulAut.conj g • fixingSubgroup (Perm α) (↑s)ᶜ
Theorem: Equiv.Perm.IwasawaT_is_conj'
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
⊢ fixingSubgroup (Perm α) (↑(g • s))ᶜ = MulAut.conj g • fixingSubgroup (Perm α) (↑s)ᶜ
Tactic:
simp only [Finset.coe_smul_finset, ← smul_compl_set]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
⊢ fixingSubgroup (Perm α) (g • (↑s)ᶜ) = MulAut.conj g • fixingSubgroup (Perm α) (↑s)ᶜ
Theorem: Equiv.Perm.IwasawaT_is_conj'
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
⊢ fixingSubgroup (Perm α) (g • (↑s)ᶜ) = MulAut.conj g • fixingSubgroup (Perm α) (↑s)ᶜ
Tactic:
apply Equiv.Perm.fixingSubgroup_conj
Proof state after:
no goals
Theorem: Equiv.Perm.IwasawaT_is_conj
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
⊢ IwasawaT (g • s) = MulAut.conj g • IwasawaT s
Tactic:
unfold IwasawaT
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
⊢ MonoidHom.range (Iwt (g • s)) = MulAut.conj g • MonoidHom.range (Iwt s)
Theorem: Equiv.Perm.IwasawaT_is_conj
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
⊢ MonoidHom.range (Iwt (g • s)) = MulAut.conj g • MonoidHom.range (Iwt s)
Tactic:
have hkg : ∀ a, a ∈ s ↔ g a ∈ g • s := by
  intro a
  rw [← Equiv.Perm.smul_def, Finset.smul_mem_smul_finset_iff]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
hkg : ∀ (a : α), a ∈ s ↔ g a ∈ g • s
⊢ MonoidHom.range (Iwt (g • s)) = MulAut.conj g • MonoidHom.range (Iwt s)
Theorem: Equiv.Perm.IwasawaT_is_conj
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
hkg : ∀ (a : α), a ∈ s ↔ g a ∈ g • s
⊢ MonoidHom.range (Iwt (g • s)) = MulAut.conj g • MonoidHom.range (Iwt s)
Tactic:
let kg : s ≃ (g • s : Finset α) := Equiv.subtypeEquiv g hkg
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
hkg : ∀ (a : α), a ∈ s ↔ g a ∈ g • s
kg : { x // x ∈ s } ≃ { x // x ∈ g • s } := subtypeEquiv g hkg
⊢ MonoidHom.range (Iwt (g • s)) = MulAut.conj g • MonoidHom.range (Iwt s)
Theorem: Equiv.Perm.IwasawaT_is_conj
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
hkg : ∀ (a : α), a ∈ s ↔ g a ∈ g • s
kg : { x // x ∈ s } ≃ { x // x ∈ g • s } := subtypeEquiv g hkg
⊢ MonoidHom.range (Iwt (g • s)) = MulAut.conj g • MonoidHom.range (Iwt s)
Tactic:
let kg' := Equiv.permCongrMul kg
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
hkg : ∀ (a : α), a ∈ s ↔ g a ∈ g • s
kg : { x // x ∈ s } ≃ { x // x ∈ g • s } := subtypeEquiv g hkg
kg' : Perm { x // x ∈ s } ≃* Perm { x // x ∈ g • s } := Equiv.permCongrMul kg
⊢ MonoidHom.range (Iwt (g • s)) = MulAut.conj g • MonoidHom.range (Iwt s)
Theorem: Equiv.Perm.IwasawaT_is_conj
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
hkg : ∀ (a : α), a ∈ s ↔ g a ∈ g • s
kg : { x // x ∈ s } ≃ { x // x ∈ g • s } := subtypeEquiv g hkg
kg' : Perm { x // x ∈ s } ≃* Perm { x // x ∈ g • s } := Equiv.permCongrMul kg
⊢ MonoidHom.range (Iwt (g • s)) = MulAut.conj g • MonoidHom.range (Iwt s)
Tactic:
suffices (Iwt (g • s)).comp kg'.toMonoidHom
  = ((MulAut.conj g).toMonoidHom.comp (Iwt s)) by
  rw [this1, ← this, ← SetLike.coe_set_eq]
  simp only [Finset.coe_sort_coe, MonoidHom.coe_range, MonoidHom.coe_comp, MulEquiv.coe_toMonoidHom,
    EquivLike.surjective_comp, EquivLike.range_comp]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
hkg : ∀ (a : α), a ∈ s ↔ g a ∈ g • s
kg : { x // x ∈ s } ≃ { x // x ∈ g • s } := subtypeEquiv g hkg
kg' : Perm { x // x ∈ s } ≃* Perm { x // x ∈ g • s } := Equiv.permCongrMul kg
⊢ MonoidHom.comp (Iwt (g • s)) (MulEquiv.toMonoidHom kg') =
    MonoidHom.comp (MulEquiv.toMonoidHom (MulAut.conj g)) (Iwt s)
Theorem: Equiv.Perm.IwasawaT_is_conj
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
hkg : ∀ (a : α), a ∈ s ↔ g a ∈ g • s
kg : { x // x ∈ s } ≃ { x // x ∈ g • s } := subtypeEquiv g hkg
kg' : Perm { x // x ∈ s } ≃* Perm { x // x ∈ g • s } := Equiv.permCongrMul kg
⊢ MonoidHom.comp (Iwt (g • s)) (MulEquiv.toMonoidHom kg') =
    MonoidHom.comp (MulEquiv.toMonoidHom (MulAut.conj g)) (Iwt s)
Tactic:
ext h x
Proof state after:
case h.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
hkg : ∀ (a : α), a ∈ s ↔ g a ∈ g • s
kg : { x // x ∈ s } ≃ { x // x ∈ g • s } := subtypeEquiv g hkg
kg' : Perm { x // x ∈ s } ≃* Perm { x // x ∈ g • s } := Equiv.permCongrMul kg
h : Perm { x // x ∈ s }
x : α
⊢ ((MonoidHom.comp (Iwt (g • s)) (MulEquiv.toMonoidHom kg')) h) x =
    ((MonoidHom.comp (MulEquiv.toMonoidHom (MulAut.conj g)) (Iwt s)) h) x
Theorem: Equiv.Perm.IwasawaT_is_conj
Proof state before:
case h.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
hkg : ∀ (a : α), a ∈ s ↔ g a ∈ g • s
kg : { x // x ∈ s } ≃ { x // x ∈ g • s } := subtypeEquiv g hkg
kg' : Perm { x // x ∈ s } ≃* Perm { x // x ∈ g • s } := Equiv.permCongrMul kg
h : Perm { x // x ∈ s }
x : α
⊢ ((MonoidHom.comp (Iwt (g • s)) (MulEquiv.toMonoidHom kg')) h) x =
    ((MonoidHom.comp (MulEquiv.toMonoidHom (MulAut.conj g)) (Iwt s)) h) x
Tactic:
unfold Iwt
Proof state after:
case h.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
hkg : ∀ (a : α), a ∈ s ↔ g a ∈ g • s
kg : { x // x ∈ s } ≃ { x // x ∈ g • s } := subtypeEquiv g hkg
kg' : Perm { x // x ∈ s } ≃* Perm { x // x ∈ g • s } := Equiv.permCongrMul kg
h : Perm { x // x ∈ s }
x : α
⊢ ((MonoidHom.comp ofSubtype (MulEquiv.toMonoidHom kg')) h) x =
    ((MonoidHom.comp (MulEquiv.toMonoidHom (MulAut.conj g)) ofSubtype) h) x
Theorem: Equiv.Perm.IwasawaT_is_conj
Proof state before:
case h.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
hkg : ∀ (a : α), a ∈ s ↔ g a ∈ g • s
kg : { x // x ∈ s } ≃ { x // x ∈ g • s } := subtypeEquiv g hkg
kg' : Perm { x // x ∈ s } ≃* Perm { x // x ∈ g • s } := Equiv.permCongrMul kg
h : Perm { x // x ∈ s }
x : α
⊢ ((MonoidHom.comp ofSubtype (MulEquiv.toMonoidHom kg')) h) x =
    ((MonoidHom.comp (MulEquiv.toMonoidHom (MulAut.conj g)) ofSubtype) h) x
Tactic:
simp only [Finset.coe_sort_coe, MonoidHom.coe_comp, MulEquiv.coe_toMonoidHom, Function.comp_apply,
  MulAut.conj_apply, coe_mul]
Proof state after:
case h.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
hkg : ∀ (a : α), a ∈ s ↔ g a ∈ g • s
kg : { x // x ∈ s } ≃ { x // x ∈ g • s } := subtypeEquiv g hkg
kg' : Perm { x // x ∈ s } ≃* Perm { x // x ∈ g • s } := Equiv.permCongrMul kg
h : Perm { x // x ∈ s }
x : α
⊢ (ofSubtype (kg' h)) x = g ((ofSubtype h) (g⁻¹ x))
Theorem: Equiv.Perm.IwasawaT_is_conj
Proof state before:
case h.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
hkg : ∀ (a : α), a ∈ s ↔ g a ∈ g • s
kg : { x // x ∈ s } ≃ { x // x ∈ g • s } := subtypeEquiv g hkg
kg' : Perm { x // x ∈ s } ≃* Perm { x // x ∈ g • s } := Equiv.permCongrMul kg
h : Perm { x // x ∈ s }
x : α
⊢ (ofSubtype (kg' h)) x = g ((ofSubtype h) (g⁻¹ x))
Tactic:
by_cases hx : g⁻¹ x ∈ s
Proof state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
hkg : ∀ (a : α), a ∈ s ↔ g a ∈ g • s
kg : { x // x ∈ s } ≃ { x // x ∈ g • s } := subtypeEquiv g hkg
kg' : Perm { x // x ∈ s } ≃* Perm { x // x ∈ g • s } := Equiv.permCongrMul kg
h : Perm { x // x ∈ s }
x : α
hx : g⁻¹ x ∈ s
⊢ (ofSubtype (kg' h)) x = g ((ofSubtype h) (g⁻¹ x))

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
hkg : ∀ (a : α), a ∈ s ↔ g a ∈ g • s
kg : { x // x ∈ s } ≃ { x // x ∈ g • s } := subtypeEquiv g hkg
kg' : Perm { x // x ∈ s } ≃* Perm { x // x ∈ g • s } := Equiv.permCongrMul kg
h : Perm { x // x ∈ s }
x : α
hx : g⁻¹ x ∉ s
⊢ (ofSubtype (kg' h)) x = g ((ofSubtype h) (g⁻¹ x))
Theorem: Equiv.Perm.IwasawaT_is_conj
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
⊢ ∀ (a : α), a ∈ s ↔ g a ∈ g • s
Tactic:
intro a
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
a : α
⊢ a ∈ s ↔ g a ∈ g • s
Theorem: Equiv.Perm.IwasawaT_is_conj
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
a : α
⊢ a ∈ s ↔ g a ∈ g • s
Tactic:
rw [← Equiv.Perm.smul_def, Finset.smul_mem_smul_finset_iff]
Proof state after:
no goals
Theorem: Equiv.Perm.IwasawaT_is_conj
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
hkg : ∀ (a : α), a ∈ s ↔ g a ∈ g • s
kg : { x // x ∈ s } ≃ { x // x ∈ g • s } := subtypeEquiv g hkg
kg' : Perm { x // x ∈ s } ≃* Perm { x // x ∈ g • s } := Equiv.permCongrMul kg
this :
  MonoidHom.comp (Iwt (g • s)) (MulEquiv.toMonoidHom kg') =
    MonoidHom.comp (MulEquiv.toMonoidHom (MulAut.conj g)) (Iwt s)
⊢ MonoidHom.range (Iwt (g • s)) = MulAut.conj g • MonoidHom.range (Iwt s)
Tactic:
rw [this1, ← this, ← SetLike.coe_set_eq]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
hkg : ∀ (a : α), a ∈ s ↔ g a ∈ g • s
kg : { x // x ∈ s } ≃ { x // x ∈ g • s } := subtypeEquiv g hkg
kg' : Perm { x // x ∈ s } ≃* Perm { x // x ∈ g • s } := Equiv.permCongrMul kg
this :
  MonoidHom.comp (Iwt (g • s)) (MulEquiv.toMonoidHom kg') =
    MonoidHom.comp (MulEquiv.toMonoidHom (MulAut.conj g)) (Iwt s)
⊢ ↑(MonoidHom.range (Iwt (g • s))) = ↑(MonoidHom.range (MonoidHom.comp (Iwt (g • s)) (MulEquiv.toMonoidHom kg')))
Theorem: Equiv.Perm.IwasawaT_is_conj
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
hkg : ∀ (a : α), a ∈ s ↔ g a ∈ g • s
kg : { x // x ∈ s } ≃ { x // x ∈ g • s } := subtypeEquiv g hkg
kg' : Perm { x // x ∈ s } ≃* Perm { x // x ∈ g • s } := Equiv.permCongrMul kg
this :
  MonoidHom.comp (Iwt (g • s)) (MulEquiv.toMonoidHom kg') =
    MonoidHom.comp (MulEquiv.toMonoidHom (MulAut.conj g)) (Iwt s)
⊢ ↑(MonoidHom.range (Iwt (g • s))) = ↑(MonoidHom.range (MonoidHom.comp (Iwt (g • s)) (MulEquiv.toMonoidHom kg')))
Tactic:
simp only [Finset.coe_sort_coe, MonoidHom.coe_range, MonoidHom.coe_comp, MulEquiv.coe_toMonoidHom,
  EquivLike.surjective_comp, EquivLike.range_comp]
Proof state after:
no goals
Theorem: Equiv.Perm.IwasawaT_is_conj
Proof state before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
hkg : ∀ (a : α), a ∈ s ↔ g a ∈ g • s
kg : { x // x ∈ s } ≃ { x // x ∈ g • s } := subtypeEquiv g hkg
kg' : Perm { x // x ∈ s } ≃* Perm { x // x ∈ g • s } := Equiv.permCongrMul kg
h : Perm { x // x ∈ s }
x : α
hx : g⁻¹ x ∈ s
⊢ (ofSubtype (kg' h)) x = g ((ofSubtype h) (g⁻¹ x))
Tactic:
suffices hx' : x ∈ g • s by
  rw [ofSubtype_apply_of_mem h hx]
  rw [ofSubtype_apply_of_mem ((Equiv.permCongrMul kg) h) hx']
  unfold Equiv.permCongrMul
  simp only [toFun_as_coe, invFun_as_coe, permCongr_symm, subtypeEquiv_symm, MulEquiv.coe_mk,
    coe_fn_mk, permCongr_apply, subtypeEquiv_apply, EmbeddingLike.apply_eq_iff_eq]
  rfl
Proof state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
hkg : ∀ (a : α), a ∈ s ↔ g a ∈ g • s
kg : { x // x ∈ s } ≃ { x // x ∈ g • s } := subtypeEquiv g hkg
kg' : Perm { x // x ∈ s } ≃* Perm { x // x ∈ g • s } := Equiv.permCongrMul kg
h : Perm { x // x ∈ s }
x : α
hx : g⁻¹ x ∈ s
⊢ x ∈ g • s
Theorem: Equiv.Perm.IwasawaT_is_conj
Proof state before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
hkg : ∀ (a : α), a ∈ s ↔ g a ∈ g • s
kg : { x // x ∈ s } ≃ { x // x ∈ g • s } := subtypeEquiv g hkg
kg' : Perm { x // x ∈ s } ≃* Perm { x // x ∈ g • s } := Equiv.permCongrMul kg
h : Perm { x // x ∈ s }
x : α
hx : g⁻¹ x ∈ s
⊢ x ∈ g • s
Tactic:
exact Finset.inv_smul_mem_iff.mp hx
Proof state after:
no goals
Theorem: Equiv.Perm.IwasawaT_is_conj
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
hkg : ∀ (a : α), a ∈ s ↔ g a ∈ g • s
kg : { x // x ∈ s } ≃ { x // x ∈ g • s } := subtypeEquiv g hkg
kg' : Perm { x // x ∈ s } ≃* Perm { x // x ∈ g • s } := Equiv.permCongrMul kg
h : Perm { x // x ∈ s }
x : α
hx : g⁻¹ x ∈ s
hx' : x ∈ g • s
⊢ (ofSubtype (kg' h)) x = g ((ofSubtype h) (g⁻¹ x))
Tactic:
rw [ofSubtype_apply_of_mem h hx]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
hkg : ∀ (a : α), a ∈ s ↔ g a ∈ g • s
kg : { x // x ∈ s } ≃ { x // x ∈ g • s } := subtypeEquiv g hkg
kg' : Perm { x // x ∈ s } ≃* Perm { x // x ∈ g • s } := Equiv.permCongrMul kg
h : Perm { x // x ∈ s }
x : α
hx : g⁻¹ x ∈ s
hx' : x ∈ g • s
⊢ (ofSubtype (kg' h)) x = g ↑(h { val := g⁻¹ x, property := hx })
Theorem: Equiv.Perm.IwasawaT_is_conj
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
hkg : ∀ (a : α), a ∈ s ↔ g a ∈ g • s
kg : { x // x ∈ s } ≃ { x // x ∈ g • s } := subtypeEquiv g hkg
kg' : Perm { x // x ∈ s } ≃* Perm { x // x ∈ g • s } := Equiv.permCongrMul kg
h : Perm { x // x ∈ s }
x : α
hx : g⁻¹ x ∈ s
hx' : x ∈ g • s
⊢ (ofSubtype (kg' h)) x = g ↑(h { val := g⁻¹ x, property := hx })
Tactic:
rw [ofSubtype_apply_of_mem ((Equiv.permCongrMul kg) h) hx']
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
hkg : ∀ (a : α), a ∈ s ↔ g a ∈ g • s
kg : { x // x ∈ s } ≃ { x // x ∈ g • s } := subtypeEquiv g hkg
kg' : Perm { x // x ∈ s } ≃* Perm { x // x ∈ g • s } := Equiv.permCongrMul kg
h : Perm { x // x ∈ s }
x : α
hx : g⁻¹ x ∈ s
hx' : x ∈ g • s
⊢ ↑(((Equiv.permCongrMul kg) h) { val := x, property := hx' }) = g ↑(h { val := g⁻¹ x, property := hx })
Theorem: Equiv.Perm.IwasawaT_is_conj
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
hkg : ∀ (a : α), a ∈ s ↔ g a ∈ g • s
kg : { x // x ∈ s } ≃ { x // x ∈ g • s } := subtypeEquiv g hkg
kg' : Perm { x // x ∈ s } ≃* Perm { x // x ∈ g • s } := Equiv.permCongrMul kg
h : Perm { x // x ∈ s }
x : α
hx : g⁻¹ x ∈ s
hx' : x ∈ g • s
⊢ ↑(((Equiv.permCongrMul kg) h) { val := x, property := hx' }) = g ↑(h { val := g⁻¹ x, property := hx })
Tactic:
unfold Equiv.permCongrMul
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
hkg : ∀ (a : α), a ∈ s ↔ g a ∈ g • s
kg : { x // x ∈ s } ≃ { x // x ∈ g • s } := subtypeEquiv g hkg
kg' : Perm { x // x ∈ s } ≃* Perm { x // x ∈ g • s } := Equiv.permCongrMul kg
h : Perm { x // x ∈ s }
x : α
hx : g⁻¹ x ∈ s
hx' : x ∈ g • s
⊢ ↑(((let __src := permCongr kg;
          { toEquiv := __src, map_mul' := ⋯ })
          h)
        { val := x, property := hx' }) =
    g ↑(h { val := g⁻¹ x, property := hx })
Theorem: Equiv.Perm.IwasawaT_is_conj
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
hkg : ∀ (a : α), a ∈ s ↔ g a ∈ g • s
kg : { x // x ∈ s } ≃ { x // x ∈ g • s } := subtypeEquiv g hkg
kg' : Perm { x // x ∈ s } ≃* Perm { x // x ∈ g • s } := Equiv.permCongrMul kg
h : Perm { x // x ∈ s }
x : α
hx : g⁻¹ x ∈ s
hx' : x ∈ g • s
⊢ ↑(((let __src := permCongr kg;
          { toEquiv := __src, map_mul' := ⋯ })
          h)
        { val := x, property := hx' }) =
    g ↑(h { val := g⁻¹ x, property := hx })
Tactic:
simp only [toFun_as_coe, invFun_as_coe, permCongr_symm, subtypeEquiv_symm, MulEquiv.coe_mk,
  coe_fn_mk, permCongr_apply, subtypeEquiv_apply, EmbeddingLike.apply_eq_iff_eq]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
hkg : ∀ (a : α), a ∈ s ↔ g a ∈ g • s
kg : { x // x ∈ s } ≃ { x // x ∈ g • s } := subtypeEquiv g hkg
kg' : Perm { x // x ∈ s } ≃* Perm { x // x ∈ g • s } := Equiv.permCongrMul kg
h : Perm { x // x ∈ s }
x : α
hx : g⁻¹ x ∈ s
hx' : x ∈ g • s
⊢ ↑(kg (h (kg.symm { val := x, property := hx' }))) = g ↑(h { val := g⁻¹ x, property := hx })