Theorem: Equiv.Perm.IwasawaT_is_conj (Jordan/PermIwasawa.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
⊢ IwasawaT (g • s) = MulAut.conj g • IwasawaT s
Tactic:
unfold IwasawaT
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)

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

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

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

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

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

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

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

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

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
⊢ ∀ (a : α), a ∈ s ↔ g a ∈ g • s
Tactic:
intro a
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
a : α
⊢ a ∈ s ↔ g a ∈ g • s

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

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

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

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

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

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

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']
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 })

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

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

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
⊢ ↑(kg (h (kg.symm { val := x, property := hx' }))) = g ↑(h { val := g⁻¹ x, property := hx })
Tactic:
rfl
State after:
no goals

State before:
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))
Tactic:
suffices hx' : x ∉ g • s by
  rw [ofSubtype_apply_of_not_mem h hx]
  rw [ofSubtype_apply_of_not_mem ((Equiv.permCongrMul kg) h) hx']
  simp only [apply_inv_self]
State after:
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
⊢ x ∉ g • s

State before:
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
⊢ x ∉ g • s
Tactic:
rw [← Finset.inv_smul_mem_iff]
State after:
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
⊢ g⁻¹ • x ∉ s

State before:
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
⊢ g⁻¹ • x ∉ s
Tactic:
exact hx
State after:
no goals

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_not_mem h hx]
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 (g⁻¹ x)

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 (g⁻¹ x)
Tactic:
rw [ofSubtype_apply_of_not_mem ((Equiv.permCongrMul kg) h) hx']
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
⊢ x = g (g⁻¹ x)

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
⊢ x = g (g⁻¹ x)
Tactic:
simp only [apply_inv_self]
State after:
no goals