[GOAL]
α : Type u_1
f g h : Perm α
⊢ Disjoint f g → Disjoint g f
[PROOFSTEP]
simp only [Disjoint, or_comm, imp_self]
[GOAL]
α : Type u_1
f g h✝ : Perm α
h : Disjoint f g
x : α
hf : ↑f x = x
hg : ↑f (↑g x) = ↑g x
⊢ ↑(f * g) x = ↑(g * f) x
[PROOFSTEP]
simp [mul_apply, hf, hg]
[GOAL]
α : Type u_1
f g h✝ : Perm α
h : Disjoint f g
x : α
hf : ↑f x = x
hg : ↑g (↑g x) = ↑g x
⊢ ↑(f * g) x = ↑(g * f) x
[PROOFSTEP]
simp [mul_apply, hf, g.injective hg]
[GOAL]
α : Type u_1
f g h✝ : Perm α
h : Disjoint f g
x : α
hg : ↑g x = x
hf : ↑f (↑f x) = ↑f x
⊢ ↑(f * g) x = ↑(g * f) x
[PROOFSTEP]
simp [mul_apply, f.injective hf, hg]
[GOAL]
α : Type u_1
f g h✝ : Perm α
h : Disjoint f g
x : α
hg : ↑g x = x
hf : ↑g (↑f x) = ↑f x
⊢ ↑(f * g) x = ↑(g * f) x
[PROOFSTEP]
simp [mul_apply, hf, hg]
[GOAL]
α : Type u_1
f g h : Perm α
⊢ Disjoint f f ↔ f = 1
[PROOFSTEP]
refine' ⟨fun h => _, fun h => h.symm ▸ disjoint_one_left 1⟩
[GOAL]
α : Type u_1
f g h✝ : Perm α
h : Disjoint f f
⊢ f = 1
[PROOFSTEP]
ext x
[GOAL]
case H
α : Type u_1
f g h✝ : Perm α
h : Disjoint f f
x : α
⊢ ↑f x = ↑1 x
[PROOFSTEP]
cases' h x with hx hx
[GOAL]
case H.inl
α : Type u_1
f g h✝ : Perm α
h : Disjoint f f
x : α
hx : ↑f x = x
⊢ ↑f x = ↑1 x
[PROOFSTEP]
simp [hx]
[GOAL]
case H.inr
α : Type u_1
f g h✝ : Perm α
h : Disjoint f f
x : α
hx : ↑f x = x
⊢ ↑f x = ↑1 x
[PROOFSTEP]
simp [hx]
[GOAL]
α : Type u_1
f g h✝ : Perm α
h : Disjoint f g
⊢ Disjoint f⁻¹ g
[PROOFSTEP]
intro x
[GOAL]
α : Type u_1
f g h✝ : Perm α
h : Disjoint f g
x : α
⊢ ↑f⁻¹ x = x ∨ ↑g x = x
[PROOFSTEP]
rw [inv_eq_iff_eq, eq_comm]
[GOAL]
α : Type u_1
f g h✝ : Perm α
h : Disjoint f g
x : α
⊢ ↑f x = x ∨ ↑g x = x
[PROOFSTEP]
exact h x
[GOAL]
α : Type u_1
f g h : Perm α
⊢ Disjoint f⁻¹ g ↔ Disjoint f g
[PROOFSTEP]
refine' ⟨fun h => _, Disjoint.inv_left⟩
[GOAL]
α : Type u_1
f g h✝ : Perm α
h : Disjoint f⁻¹ g
⊢ Disjoint f g
[PROOFSTEP]
convert h.inv_left
[GOAL]
α : Type u_1
f g h : Perm α
⊢ Disjoint f g⁻¹ ↔ Disjoint f g
[PROOFSTEP]
rw [disjoint_comm, disjoint_inv_left_iff, disjoint_comm]
[GOAL]
α : Type u_1
f g h : Perm α
H1 : Disjoint f h
H2 : Disjoint g h
x : α
⊢ ↑(f * g) x = x ∨ ↑h x = x
[PROOFSTEP]
cases H1 x
[GOAL]
case inl
α : Type u_1
f g h : Perm α
H1 : Disjoint f h
H2 : Disjoint g h
x : α
h✝ : ↑f x = x
⊢ ↑(f * g) x = x ∨ ↑h x = x
[PROOFSTEP]
cases H2 x
[GOAL]
case inr
α : Type u_1
f g h : Perm α
H1 : Disjoint f h
H2 : Disjoint g h
x : α
h✝ : ↑h x = x
⊢ ↑(f * g) x = x ∨ ↑h x = x
[PROOFSTEP]
cases H2 x
[GOAL]
case inl.inl
α : Type u_1
f g h : Perm α
H1 : Disjoint f h
H2 : Disjoint g h
x : α
h✝¹ : ↑f x = x
h✝ : ↑g x = x
⊢ ↑(f * g) x = x ∨ ↑h x = x
[PROOFSTEP]
simp [*]
[GOAL]
case inl.inr
α : Type u_1
f g h : Perm α
H1 : Disjoint f h
H2 : Disjoint g h
x : α
h✝¹ : ↑f x = x
h✝ : ↑h x = x
⊢ ↑(f * g) x = x ∨ ↑h x = x
[PROOFSTEP]
simp [*]
[GOAL]
case inr.inl
α : Type u_1
f g h : Perm α
H1 : Disjoint f h
H2 : Disjoint g h
x : α
h✝¹ : ↑h x = x
h✝ : ↑g x = x
⊢ ↑(f * g) x = x ∨ ↑h x = x
[PROOFSTEP]
simp [*]
[GOAL]
case inr.inr
α : Type u_1
f g h : Perm α
H1 : Disjoint f h
H2 : Disjoint g h
x : α
h✝¹ h✝ : ↑h x = x
⊢ ↑(f * g) x = x ∨ ↑h x = x
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
f g h : Perm α
H1 : Disjoint f g
H2 : Disjoint f h
⊢ Disjoint f (g * h)
[PROOFSTEP]
rw [disjoint_comm]
[GOAL]
α : Type u_1
f g h : Perm α
H1 : Disjoint f g
H2 : Disjoint f h
⊢ Disjoint (g * h) f
[PROOFSTEP]
exact H1.symm.mul_left H2.symm
[GOAL]
α : Type u_1
f g h✝ h : Perm α
x✝ : α
⊢ ↑(h * f * h⁻¹) x✝ = x✝ ∨ ↑(h * g * h⁻¹) x✝ = x✝ ↔ ↑f (↑h⁻¹ x✝) = ↑h⁻¹ x✝ ∨ ↑g (↑h⁻¹ x✝) = ↑h⁻¹ x✝
[PROOFSTEP]
simp only [mul_apply, eq_inv_iff_eq]
[GOAL]
α : Type u_1
f g h✝ : Perm α
l : List (Perm α)
h : ∀ (g : Perm α), g ∈ l → Disjoint f g
⊢ Disjoint f (List.prod l)
[PROOFSTEP]
induction' l with g l ih
[GOAL]
case nil
α : Type u_1
f g h✝¹ : Perm α
l : List (Perm α)
h✝ : ∀ (g : Perm α), g ∈ l → Disjoint f g
h : ∀ (g : Perm α), g ∈ [] → Disjoint f g
⊢ Disjoint f (List.prod [])
[PROOFSTEP]
exact disjoint_one_right _
[GOAL]
case cons
α : Type u_1
f g✝ h✝¹ : Perm α
l✝ : List (Perm α)
h✝ : ∀ (g : Perm α), g ∈ l✝ → Disjoint f g
g : Perm α
l : List (Perm α)
ih : (∀ (g : Perm α), g ∈ l → Disjoint f g) → Disjoint f (List.prod l)
h : ∀ (g_1 : Perm α), g_1 ∈ g :: l → Disjoint f g_1
⊢ Disjoint f (List.prod (g :: l))
[PROOFSTEP]
rw [List.prod_cons]
[GOAL]
case cons
α : Type u_1
f g✝ h✝¹ : Perm α
l✝ : List (Perm α)
h✝ : ∀ (g : Perm α), g ∈ l✝ → Disjoint f g
g : Perm α
l : List (Perm α)
ih : (∀ (g : Perm α), g ∈ l → Disjoint f g) → Disjoint f (List.prod l)
h : ∀ (g_1 : Perm α), g_1 ∈ g :: l → Disjoint f g_1
⊢ Disjoint f (g * List.prod l)
[PROOFSTEP]
exact (h _ (List.mem_cons_self _ _)).mul_right (ih fun g hg => h g (List.mem_cons_of_mem _ hg))
[GOAL]
α : Type u_1
f g h : Perm α
l : List (Perm α)
h1 : ¬1 ∈ l
h2 : List.Pairwise Disjoint l
⊢ List.Nodup l
[PROOFSTEP]
refine' List.Pairwise.imp_of_mem _ h2
[GOAL]
α : Type u_1
f g h : Perm α
l : List (Perm α)
h1 : ¬1 ∈ l
h2 : List.Pairwise Disjoint l
⊢ ∀ {a b : Perm α}, a ∈ l → b ∈ l → Disjoint a b → a ≠ b
[PROOFSTEP]
intro τ σ h_mem _ h_disjoint _
[GOAL]
α : Type u_1
f g h : Perm α
l : List (Perm α)
h1 : ¬1 ∈ l
h2 : List.Pairwise Disjoint l
τ σ : Perm α
h_mem : τ ∈ l
a✝¹ : σ ∈ l
h_disjoint : Disjoint τ σ
a✝ : τ = σ
⊢ False
[PROOFSTEP]
subst τ
[GOAL]
α : Type u_1
f g h : Perm α
l : List (Perm α)
h1 : ¬1 ∈ l
h2 : List.Pairwise Disjoint l
σ : Perm α
a✝ h_mem : σ ∈ l
h_disjoint : Disjoint σ σ
⊢ False
[PROOFSTEP]
suffices (σ : Perm α) = 1 by
  rw [this] at h_mem
  exact h1 h_mem
[GOAL]
α : Type u_1
f g h : Perm α
l : List (Perm α)
h1 : ¬1 ∈ l
h2 : List.Pairwise Disjoint l
σ : Perm α
a✝ h_mem : σ ∈ l
h_disjoint : Disjoint σ σ
this : σ = 1
⊢ False
[PROOFSTEP]
rw [this] at h_mem
[GOAL]
α : Type u_1
f g h : Perm α
l : List (Perm α)
h1 : ¬1 ∈ l
h2 : List.Pairwise Disjoint l
σ : Perm α
a✝ : σ ∈ l
h_mem : 1 ∈ l
h_disjoint : Disjoint σ σ
this : σ = 1
⊢ False
[PROOFSTEP]
exact h1 h_mem
[GOAL]
α : Type u_1
f g h : Perm α
l : List (Perm α)
h1 : ¬1 ∈ l
h2 : List.Pairwise Disjoint l
σ : Perm α
a✝ h_mem : σ ∈ l
h_disjoint : Disjoint σ σ
⊢ σ = 1
[PROOFSTEP]
exact ext fun a => (or_self_iff _).mp (h_disjoint a)
[GOAL]
α : Type u_1
f g h : Perm α
x : α
hfx : ↑f x = x
n : ℕ
⊢ ↑(f ^ (n + 1)) x = x
[PROOFSTEP]
rw [pow_succ', mul_apply, hfx, pow_apply_eq_self_of_apply_eq_self hfx n]
[GOAL]
α : Type u_1
f g h : Perm α
x : α
hfx : ↑f x = x
n : ℕ
⊢ ↑(f ^ Int.negSucc n) x = x
[PROOFSTEP]
rw [zpow_negSucc, inv_eq_iff_eq, pow_apply_eq_self_of_apply_eq_self hfx]
[GOAL]
α : Type u_1
f g h✝ : Perm α
x : α
hffx : ↑f (↑f x) = x
n : ℕ
h : ↑(f ^ n) x = x
⊢ ↑(f ^ (n + 1)) x = ↑f x
[PROOFSTEP]
rw [pow_succ, mul_apply, h]
[GOAL]
α : Type u_1
f g h✝ : Perm α
x : α
hffx : ↑f (↑f x) = x
n : ℕ
h : ↑(f ^ n) x = ↑f x
⊢ ↑(f ^ (n + 1)) x = x
[PROOFSTEP]
rw [pow_succ, mul_apply, h, hffx]
[GOAL]
α : Type u_1
f g h : Perm α
x : α
hffx : ↑f (↑f x) = x
n : ℕ
⊢ ↑(f ^ Int.negSucc n) x = x ∨ ↑(f ^ Int.negSucc n) x = ↑f x
[PROOFSTEP]
rw [zpow_negSucc, inv_eq_iff_eq, ← f.injective.eq_iff, ← mul_apply, ← pow_succ, eq_comm, inv_eq_iff_eq, ← mul_apply, ←
  pow_succ', @eq_comm _ x, or_comm]
[GOAL]
α : Type u_1
f g h : Perm α
x : α
hffx : ↑f (↑f x) = x
n : ℕ
⊢ ↑(f ^ (n + 1 + 1)) x = x ∨ ↑(f ^ (n + 1 + 1)) x = ↑f x
[PROOFSTEP]
exact pow_apply_eq_of_apply_apply_eq_self hffx _
[GOAL]
α : Type u_1
f g h σ τ : Perm α
hστ : Disjoint σ τ
a : α
⊢ ↑(σ * τ) a = a ↔ ↑σ a = a ∧ ↑τ a = a
[PROOFSTEP]
refine' ⟨fun h => _, fun h => by rw [mul_apply, h.2, h.1]⟩
[GOAL]
α : Type u_1
f g h✝ σ τ : Perm α
hστ : Disjoint σ τ
a : α
h : ↑σ a = a ∧ ↑τ a = a
⊢ ↑(σ * τ) a = a
[PROOFSTEP]
rw [mul_apply, h.2, h.1]
[GOAL]
α : Type u_1
f g h✝ σ τ : Perm α
hστ : Disjoint σ τ
a : α
h : ↑(σ * τ) a = a
⊢ ↑σ a = a ∧ ↑τ a = a
[PROOFSTEP]
cases' hστ a with hσ hτ
[GOAL]
case inl
α : Type u_1
f g h✝ σ τ : Perm α
hστ : Disjoint σ τ
a : α
h : ↑(σ * τ) a = a
hσ : ↑σ a = a
⊢ ↑σ a = a ∧ ↑τ a = a
[PROOFSTEP]
exact ⟨hσ, σ.injective (h.trans hσ.symm)⟩
[GOAL]
case inr
α : Type u_1
f g h✝ σ τ : Perm α
hστ : Disjoint σ τ
a : α
h : ↑(σ * τ) a = a
hτ : ↑τ a = a
⊢ ↑σ a = a ∧ ↑τ a = a
[PROOFSTEP]
exact ⟨(congr_arg σ hτ).symm.trans h, hτ⟩
[GOAL]
α : Type u_1
f g h σ τ : Perm α
hστ : Disjoint σ τ
⊢ σ * τ = 1 ↔ σ = 1 ∧ τ = 1
[PROOFSTEP]
simp_rw [ext_iff, one_apply, hστ.mul_apply_eq_iff, forall_and]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
⊢ ↑(↑ofSubtype (swap x y)) z = ↑(swap ↑x ↑y) z
[PROOFSTEP]
by_cases hz : p z
[GOAL]
case pos
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : p z
⊢ ↑(↑ofSubtype (swap x y)) z = ↑(swap ↑x ↑y) z
[PROOFSTEP]
rw [swap_apply_def, ofSubtype_apply_of_mem _ hz]
[GOAL]
case pos
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : p z
⊢ ↑(↑(swap x y) { val := z, property := hz }) = if z = ↑x then ↑y else if z = ↑y then ↑x else z
[PROOFSTEP]
split_ifs with hzx hzy
[GOAL]
case pos
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : p z
hzx : z = ↑x
⊢ ↑(↑(swap x y) { val := z, property := hz }) = ↑y
[PROOFSTEP]
simp_rw [hzx, Subtype.coe_eta, swap_apply_left]
[GOAL]
case pos
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : p z
hzx : ¬z = ↑x
hzy : z = ↑y
⊢ ↑(↑(swap x y) { val := z, property := hz }) = ↑x
[PROOFSTEP]
simp_rw [hzy, Subtype.coe_eta, swap_apply_right]
[GOAL]
case neg
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : p z
hzx : ¬z = ↑x
hzy : ¬z = ↑y
⊢ ↑(↑(swap x y) { val := z, property := hz }) = z
[PROOFSTEP]
rw [swap_apply_of_ne_of_ne]
[GOAL]
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : p z
hzx : ¬z = ↑x
hzy : ¬z = ↑y
⊢ { val := z, property := hz } ≠ x
[PROOFSTEP]
simp [Subtype.ext_iff, *]
[GOAL]
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : p z
hzx : ¬z = ↑x
hzy : ¬z = ↑y
⊢ { val := z, property := hz } ≠ y
[PROOFSTEP]
simp [Subtype.ext_iff, *]
[GOAL]
case neg
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : ¬p z
⊢ ↑(↑ofSubtype (swap x y)) z = ↑(swap ↑x ↑y) z
[PROOFSTEP]
rw [ofSubtype_apply_of_not_mem _ hz, swap_apply_of_ne_of_ne]
[GOAL]
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : ¬p z
⊢ z ≠ ↑x
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : ¬p z
⊢ z ≠ ↑y
[PROOFSTEP]
intro h
[GOAL]
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : ¬p z
h : z = ↑x
⊢ False
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : ¬p z
⊢ z ≠ ↑y
[PROOFSTEP]
apply hz
[GOAL]
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : ¬p z
h : z = ↑x
⊢ p z
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : ¬p z
⊢ z ≠ ↑y
[PROOFSTEP]
rw [h]
[GOAL]
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : ¬p z
h : z = ↑x
⊢ p ↑x
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : ¬p z
⊢ z ≠ ↑y
[PROOFSTEP]
exact Subtype.prop x
[GOAL]
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : ¬p z
⊢ z ≠ ↑y
[PROOFSTEP]
intro h
[GOAL]
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : ¬p z
h : z = ↑y
⊢ False
[PROOFSTEP]
apply hz
[GOAL]
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : ¬p z
h : z = ↑y
⊢ p z
[PROOFSTEP]
rw [h]
[GOAL]
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : ¬p z
h : z = ↑y
⊢ p ↑y
[PROOFSTEP]
exact Subtype.prop y
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
h : IsSwap f
x : α
hx : p x
y : α
hy : p y
hxy :
  { val := x, property := hx } ≠ { val := y, property := hy } ∧
    f = swap { val := x, property := hx } { val := y, property := hy }
⊢ x ≠ y
[PROOFSTEP]
simp only [Ne.def, Subtype.ext_iff] at hxy
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
h : IsSwap f
x : α
hx : p x
y : α
hy : p y
hxy : ¬x = y ∧ f = swap { val := x, property := hx } { val := y, property := hy }
⊢ x ≠ y
[PROOFSTEP]
exact hxy.1
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
h : IsSwap f
x : α
hx : p x
y : α
hy : p y
hxy :
  { val := x, property := hx } ≠ { val := y, property := hy } ∧
    f = swap { val := x, property := hx } { val := y, property := hy }
⊢ ↑ofSubtype f = swap x y
[PROOFSTEP]
rw [hxy.2, ofSubtype_swap_eq]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
hy : ↑(swap x (↑f x) * f) y ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
simp only [swap_apply_def, mul_apply, f.injective.eq_iff] at *
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
hy : (if ↑f y = x then ↑f x else if y = x then x else ↑f y) ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
by_cases h : f y = x
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
hy : (if ↑f y = x then ↑f x else if y = x then x else ↑f y) ≠ y
h : ↑f y = x
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
constructor
[GOAL]
case pos.left
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
hy : (if ↑f y = x then ↑f x else if y = x then x else ↑f y) ≠ y
h : ↑f y = x
⊢ ↑f y ≠ y
[PROOFSTEP]
intro
[GOAL]
case pos.right
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
hy : (if ↑f y = x then ↑f x else if y = x then x else ↑f y) ≠ y
h : ↑f y = x
⊢ y ≠ x
[PROOFSTEP]
intro
[GOAL]
case pos.left
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
hy : (if ↑f y = x then ↑f x else if y = x then x else ↑f y) ≠ y
h : ↑f y = x
a✝ : ↑f y = y
⊢ False
[PROOFSTEP]
simp_all only [if_true, eq_self_iff_true, not_true, Ne.def]
[GOAL]
case pos.right
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
hy : (if ↑f y = x then ↑f x else if y = x then x else ↑f y) ≠ y
h : ↑f y = x
a✝ : y = x
⊢ False
[PROOFSTEP]
simp_all only [if_true, eq_self_iff_true, not_true, Ne.def]
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
hy : (if ↑f y = x then ↑f x else if y = x then x else ↑f y) ≠ y
h : ¬↑f y = x
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
split_ifs at hy  with h h
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
h✝ : ¬↑f y = x
h : ↑f y = x
hy : ↑f x ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
try {subst x
}
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
h✝ : ¬↑f y = x
h : ↑f y = x
hy : ↑f x ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
{subst x
}
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
h✝ : ¬↑f y = x
h : ↑f y = x
hy : ↑f x ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
subst x
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
h✝¹ : ¬↑f y = x
h✝ : ¬↑f y = x
h : y = x
hy : x ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
try {subst x
}
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
h✝¹ : ¬↑f y = x
h✝ : ¬↑f y = x
h : y = x
hy : x ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
{subst x
}
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
h✝¹ : ¬↑f y = x
h✝ : ¬↑f y = x
h : y = x
hy : x ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
subst x
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
h✝¹ : ¬↑f y = x
h✝ : ¬↑f y = x
h : ¬y = x
hy : ↑f y ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
try {subst x
}
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
h✝¹ : ¬↑f y = x
h✝ : ¬↑f y = x
h : ¬y = x
hy : ↑f y ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
{subst x
}
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
h✝¹ : ¬↑f y = x
h✝ : ¬↑f y = x
h : ¬y = x
hy : ↑f y ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
subst x
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
h✝ : ¬↑f y = x
h : ↑f y = x
hy : ↑f x ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
try {simp [*] at *
}
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
h✝ : ¬↑f y = x
h : ↑f y = x
hy : ↑f x ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
{simp [*] at *
}
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
h✝ : ¬↑f y = x
h : ↑f y = x
hy : ↑f x ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
simp [*] at *
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
h✝¹ : ¬↑f y = x
h✝ : ¬↑f y = x
h : y = x
hy : x ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
try {simp [*] at *
}
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
h✝¹ : ¬↑f y = x
h✝ : ¬↑f y = x
h : y = x
hy : x ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
{simp [*] at *
}
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
h✝¹ : ¬↑f y = x
h✝ : ¬↑f y = x
h : y = x
hy : x ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
simp [*] at *
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
h✝¹ : ¬↑f y = x
h✝ : ¬↑f y = x
h : ¬y = x
hy : ↑f y ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
try {simp [*] at *
}
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
h✝¹ : ¬↑f y = x
h✝ : ¬↑f y = x
h : ¬y = x
hy : ↑f y ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
{simp [*] at *
}
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
h✝¹ : ¬↑f y = x
h✝ : ¬↑f y = x
h : ¬y = x
hy : ↑f y ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
simp [*] at *
[GOAL]
α : Type u_1
p q : Perm α
⊢ {x | ↑p⁻¹ x ≠ x} = {x | ↑p x ≠ x}
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
p q : Perm α
x : α
⊢ x ∈ {x | ↑p⁻¹ x ≠ x} ↔ x ∈ {x | ↑p x ≠ x}
[PROOFSTEP]
simp only [Set.mem_setOf_eq, Ne.def]
[GOAL]
case h
α : Type u_1
p q : Perm α
x : α
⊢ ¬↑p⁻¹ x = x ↔ ¬↑p x = x
[PROOFSTEP]
rw [inv_def, symm_apply_eq, eq_comm]
[GOAL]
α : Type u_1
p✝ q p : Perm α
a : α
⊢ ↑p a ∈ {x | ↑p x ≠ x} ↔ a ∈ {x | ↑p x ≠ x}
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
p q : Perm α
n : ℤ
⊢ {x | ↑(p ^ n) x ≠ x} ⊆ {x | ↑p x ≠ x}
[PROOFSTEP]
intro x
[GOAL]
α : Type u_1
p q : Perm α
n : ℤ
x : α
⊢ x ∈ {x | ↑(p ^ n) x ≠ x} → x ∈ {x | ↑p x ≠ x}
[PROOFSTEP]
simp only [Set.mem_setOf_eq, Ne.def]
[GOAL]
α : Type u_1
p q : Perm α
n : ℤ
x : α
⊢ ¬↑(p ^ n) x = x → ¬↑p x = x
[PROOFSTEP]
intro hx H
[GOAL]
α : Type u_1
p q : Perm α
n : ℤ
x : α
hx : ¬↑(p ^ n) x = x
H : ↑p x = x
⊢ False
[PROOFSTEP]
simp [zpow_apply_eq_self_of_apply_eq_self H] at hx
[GOAL]
α : Type u_1
p q : Perm α
⊢ {x | ↑(p * q) x ≠ x} ⊆ {x | ↑p x ≠ x} ∪ {x | ↑q x ≠ x}
[PROOFSTEP]
intro x
[GOAL]
α : Type u_1
p q : Perm α
x : α
⊢ x ∈ {x | ↑(p * q) x ≠ x} → x ∈ {x | ↑p x ≠ x} ∪ {x | ↑q x ≠ x}
[PROOFSTEP]
simp only [Perm.coe_mul, Function.comp_apply, Ne.def, Set.mem_union, Set.mem_setOf_eq]
[GOAL]
α : Type u_1
p q : Perm α
x : α
⊢ ¬↑p (↑q x) = x → ¬↑p x = x ∨ ¬↑q x = x
[PROOFSTEP]
by_cases hq : q x = x
[GOAL]
case pos
α : Type u_1
p q : Perm α
x : α
hq : ↑q x = x
⊢ ¬↑p (↑q x) = x → ¬↑p x = x ∨ ¬↑q x = x
[PROOFSTEP]
simp [hq]
[GOAL]
case neg
α : Type u_1
p q : Perm α
x : α
hq : ¬↑q x = x
⊢ ¬↑p (↑q x) = x → ¬↑p x = x ∨ ¬↑q x = x
[PROOFSTEP]
simp [hq]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x : α
⊢ x ∈ support f ↔ ↑f x ≠ x
[PROOFSTEP]
rw [support, mem_filter, and_iff_right (mem_univ x)]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x : α
⊢ ¬x ∈ support f ↔ ↑f x = x
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
⊢ ↑(support f) = {x | ↑f x ≠ x}
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x✝ : α
⊢ x✝ ∈ ↑(support f) ↔ x✝ ∈ {x | ↑f x ≠ x}
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g σ : Perm α
⊢ support σ = ∅ ↔ σ = 1
[PROOFSTEP]
simp_rw [Finset.ext_iff, mem_support, Finset.not_mem_empty, iff_false_iff, not_not, Equiv.Perm.ext_iff, one_apply]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
⊢ support 1 = ∅
[PROOFSTEP]
rw [support_eq_empty_iff]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : support f ⊆ support g
h' : ∀ (x : α), x ∈ support g → ↑f x = ↑g x
⊢ f = g
[PROOFSTEP]
ext x
[GOAL]
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : support f ⊆ support g
h' : ∀ (x : α), x ∈ support g → ↑f x = ↑g x
x : α
⊢ ↑f x = ↑g x
[PROOFSTEP]
by_cases hx : x ∈ g.support
[GOAL]
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : support f ⊆ support g
h' : ∀ (x : α), x ∈ support g → ↑f x = ↑g x
x : α
hx : x ∈ support g
⊢ ↑f x = ↑g x
[PROOFSTEP]
exact h' x hx
[GOAL]
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : support f ⊆ support g
h' : ∀ (x : α), x ∈ support g → ↑f x = ↑g x
x : α
hx : ¬x ∈ support g
⊢ ↑f x = ↑g x
[PROOFSTEP]
rw [not_mem_support.mp hx, ← not_mem_support]
[GOAL]
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : support f ⊆ support g
h' : ∀ (x : α), x ∈ support g → ↑f x = ↑g x
x : α
hx : ¬x ∈ support g
⊢ ¬x ∈ support f
[PROOFSTEP]
exact fun H => hx (h H)
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g✝ f g : Perm α
x : α
⊢ x ∈ support (f * g) → x ∈ support f ⊔ support g
[PROOFSTEP]
simp only [sup_eq_union]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g✝ f g : Perm α
x : α
⊢ x ∈ support (f * g) → x ∈ support f ∪ support g
[PROOFSTEP]
rw [mem_union, mem_support, mem_support, mem_support, mul_apply, ← not_and_or, not_imp_not]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g✝ f g : Perm α
x : α
⊢ ↑f x = x ∧ ↑g x = x → ↑f (↑g x) = x
[PROOFSTEP]
rintro ⟨hf, hg⟩
[GOAL]
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g✝ f g : Perm α
x : α
hf : ↑f x = x
hg : ↑g x = x
⊢ ↑f (↑g x) = x
[PROOFSTEP]
rw [hg, hf]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
x : α
hx : x ∈ support (List.prod l)
⊢ ∃ f, f ∈ l ∧ x ∈ support f
[PROOFSTEP]
contrapose! hx
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
x : α
hx : ∀ (f : Perm α), f ∈ l → ¬x ∈ support f
⊢ ¬x ∈ support (List.prod l)
[PROOFSTEP]
simp_rw [mem_support, not_not] at hx ⊢
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
x : α
hx : ∀ (f : Perm α), f ∈ l → ↑f x = x
⊢ ↑(List.prod l) x = x
[PROOFSTEP]
induction' l with f l ih
[GOAL]
case nil
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
x : α
hx✝ : ∀ (f : Perm α), f ∈ l → ↑f x = x
hx : ∀ (f : Perm α), f ∈ [] → ↑f x = x
⊢ ↑(List.prod []) x = x
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
l✝ : List (Perm α)
x : α
hx✝ : ∀ (f : Perm α), f ∈ l✝ → ↑f x = x
f : Perm α
l : List (Perm α)
ih : (∀ (f : Perm α), f ∈ l → ↑f x = x) → ↑(List.prod l) x = x
hx : ∀ (f_1 : Perm α), f_1 ∈ f :: l → ↑f_1 x = x
⊢ ↑(List.prod (f :: l)) x = x
[PROOFSTEP]
rw [List.prod_cons, mul_apply, ih, hx]
[GOAL]
case cons._
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
l✝ : List (Perm α)
x : α
hx✝ : ∀ (f : Perm α), f ∈ l✝ → ↑f x = x
f : Perm α
l : List (Perm α)
ih : (∀ (f : Perm α), f ∈ l → ↑f x = x) → ↑(List.prod l) x = x
hx : ∀ (f_1 : Perm α), f_1 ∈ f :: l → ↑f_1 x = x
⊢ f ∈ f :: l
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
l✝ : List (Perm α)
x : α
hx✝ : ∀ (f : Perm α), f ∈ l✝ → ↑f x = x
f : Perm α
l : List (Perm α)
ih : (∀ (f : Perm α), f ∈ l → ↑f x = x) → ↑(List.prod l) x = x
hx : ∀ (f_1 : Perm α), f_1 ∈ f :: l → ↑f_1 x = x
⊢ ∀ (f : Perm α), f ∈ l → ↑f x = x
[PROOFSTEP]
simp only [List.find?, List.mem_cons, true_or]
[GOAL]
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
l✝ : List (Perm α)
x : α
hx✝ : ∀ (f : Perm α), f ∈ l✝ → ↑f x = x
f : Perm α
l : List (Perm α)
ih : (∀ (f : Perm α), f ∈ l → ↑f x = x) → ↑(List.prod l) x = x
hx : ∀ (f_1 : Perm α), f_1 ∈ f :: l → ↑f_1 x = x
⊢ ∀ (f : Perm α), f ∈ l → ↑f x = x
[PROOFSTEP]
intros f' hf'
[GOAL]
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
l✝ : List (Perm α)
x : α
hx✝ : ∀ (f : Perm α), f ∈ l✝ → ↑f x = x
f : Perm α
l : List (Perm α)
ih : (∀ (f : Perm α), f ∈ l → ↑f x = x) → ↑(List.prod l) x = x
hx : ∀ (f_1 : Perm α), f_1 ∈ f :: l → ↑f_1 x = x
f' : Perm α
hf' : f' ∈ l
⊢ ↑f' x = x
[PROOFSTEP]
refine' hx f' _
[GOAL]
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
l✝ : List (Perm α)
x : α
hx✝ : ∀ (f : Perm α), f ∈ l✝ → ↑f x = x
f : Perm α
l : List (Perm α)
ih : (∀ (f : Perm α), f ∈ l → ↑f x = x) → ↑(List.prod l) x = x
hx : ∀ (f_1 : Perm α), f_1 ∈ f :: l → ↑f_1 x = x
f' : Perm α
hf' : f' ∈ l
⊢ f' ∈ f :: l
[PROOFSTEP]
simp only [List.find?, List.mem_cons]
[GOAL]
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
l✝ : List (Perm α)
x : α
hx✝ : ∀ (f : Perm α), f ∈ l✝ → ↑f x = x
f : Perm α
l : List (Perm α)
ih : (∀ (f : Perm α), f ∈ l → ↑f x = x) → ↑(List.prod l) x = x
hx : ∀ (f_1 : Perm α), f_1 ∈ f :: l → ↑f_1 x = x
f' : Perm α
hf' : f' ∈ l
⊢ f' = f ∨ f' ∈ l
[PROOFSTEP]
exact Or.inr hf'
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g σ : Perm α
⊢ support σ⁻¹ = support σ
[PROOFSTEP]
simp_rw [Finset.ext_iff, mem_support, not_iff_not, inv_eq_iff_eq.trans eq_comm, imp_true_iff]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x : α
⊢ ↑f x ∈ support f ↔ x ∈ support f
[PROOFSTEP]
rw [mem_support, mem_support, Ne.def, Ne.def, apply_eq_iff_eq]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
n : ℕ
x : α
⊢ ↑f (↑(f ^ n) x) = ↑(f ^ n) x ↔ ↑f x = x
[PROOFSTEP]
rw [← mul_apply, Commute.self_pow f, mul_apply, apply_eq_iff_eq]
  -- @[simp] -- Porting note: simp can prove this
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
n : ℕ
x : α
⊢ ↑(f ^ n) x ∈ support f ↔ x ∈ support f
[PROOFSTEP]
simp only [mem_support, ne_eq, apply_pow_apply_eq_iff]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
n : ℤ
x : α
⊢ ↑f (↑(f ^ n) x) = ↑(f ^ n) x ↔ ↑f x = x
[PROOFSTEP]
rw [← mul_apply, Commute.self_zpow f, mul_apply, apply_eq_iff_eq]
  -- @[simp] -- Porting note: simp can prove this
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
n : ℤ
x : α
⊢ ↑(f ^ n) x ∈ support f ↔ x ∈ support f
[PROOFSTEP]
simp only [mem_support, ne_eq, apply_zpow_apply_eq_iff]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : ∀ (x : α), x ∈ support f ∩ support g → ↑f x = ↑g x
k : ℕ
⊢ ∀ (x : α), x ∈ support f ∩ support g → ↑(f ^ k) x = ↑(g ^ k) x
[PROOFSTEP]
induction' k with k hk
[GOAL]
case zero
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : ∀ (x : α), x ∈ support f ∩ support g → ↑f x = ↑g x
⊢ ∀ (x : α), x ∈ support f ∩ support g → ↑(f ^ Nat.zero) x = ↑(g ^ Nat.zero) x
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : ∀ (x : α), x ∈ support f ∩ support g → ↑f x = ↑g x
k : ℕ
hk : ∀ (x : α), x ∈ support f ∩ support g → ↑(f ^ k) x = ↑(g ^ k) x
⊢ ∀ (x : α), x ∈ support f ∩ support g → ↑(f ^ Nat.succ k) x = ↑(g ^ Nat.succ k) x
[PROOFSTEP]
intro x hx
[GOAL]
case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : ∀ (x : α), x ∈ support f ∩ support g → ↑f x = ↑g x
k : ℕ
hk : ∀ (x : α), x ∈ support f ∩ support g → ↑(f ^ k) x = ↑(g ^ k) x
x : α
hx : x ∈ support f ∩ support g
⊢ ↑(f ^ Nat.succ k) x = ↑(g ^ Nat.succ k) x
[PROOFSTEP]
rw [pow_succ', mul_apply, pow_succ', mul_apply, h _ hx, hk]
[GOAL]
case succ.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : ∀ (x : α), x ∈ support f ∩ support g → ↑f x = ↑g x
k : ℕ
hk : ∀ (x : α), x ∈ support f ∩ support g → ↑(f ^ k) x = ↑(g ^ k) x
x : α
hx : x ∈ support f ∩ support g
⊢ ↑g x ∈ support f ∩ support g
[PROOFSTEP]
rwa [mem_inter, apply_mem_support, ← h _ hx, apply_mem_support, ← mem_inter]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
⊢ Disjoint f g ↔ _root_.Disjoint (support f) (support g)
[PROOFSTEP]
simp [disjoint_iff_eq_or_eq, disjoint_iff, disjoint_iff, Finset.ext_iff, not_and_or, imp_iff_not_or]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : Disjoint f g
⊢ support (f * g) = support f ∪ support g
[PROOFSTEP]
refine' le_antisymm (support_mul_le _ _) fun a => _
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : Disjoint f g
a : α
⊢ a ∈ support f ∪ support g → a ∈ support (f * g)
[PROOFSTEP]
rw [mem_union, mem_support, mem_support, mem_support, mul_apply, ← not_and_or, not_imp_not]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : Disjoint f g
a : α
⊢ ↑f (↑g a) = a → ↑f a = a ∧ ↑g a = a
[PROOFSTEP]
exact
  (h a).elim (fun hf h => ⟨hf, f.apply_eq_iff_eq.mp (h.trans hf.symm)⟩) fun hg h => ⟨(congr_arg f hg).symm.trans h, hg⟩
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h : List.Pairwise Disjoint l
⊢ support (List.prod l) = List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support l)
[PROOFSTEP]
induction' l with hd tl hl
[GOAL]
case nil
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : List.Pairwise Disjoint l
h : List.Pairwise Disjoint []
⊢ support (List.prod []) = List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support [])
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : List.Pairwise Disjoint l
hd : Perm α
tl : List (Perm α)
hl : List.Pairwise Disjoint tl → support (List.prod tl) = List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support tl)
h : List.Pairwise Disjoint (hd :: tl)
⊢ support (List.prod (hd :: tl)) = List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support (hd :: tl))
[PROOFSTEP]
rw [List.pairwise_cons] at h
[GOAL]
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : List.Pairwise Disjoint l
hd : Perm α
tl : List (Perm α)
hl : List.Pairwise Disjoint tl → support (List.prod tl) = List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support tl)
h : (∀ (a' : Perm α), a' ∈ tl → Disjoint hd a') ∧ List.Pairwise Disjoint tl
⊢ support (List.prod (hd :: tl)) = List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support (hd :: tl))
[PROOFSTEP]
have : Disjoint hd tl.prod := disjoint_prod_right _ h.left
[GOAL]
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : List.Pairwise Disjoint l
hd : Perm α
tl : List (Perm α)
hl : List.Pairwise Disjoint tl → support (List.prod tl) = List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support tl)
h : (∀ (a' : Perm α), a' ∈ tl → Disjoint hd a') ∧ List.Pairwise Disjoint tl
this : Disjoint hd (List.prod tl)
⊢ support (List.prod (hd :: tl)) = List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support (hd :: tl))
[PROOFSTEP]
simp [this.support_mul, hl h.right]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
⊢ support (List.prod l) ≤ List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support l)
[PROOFSTEP]
induction' l with hd tl hl
[GOAL]
case nil
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
⊢ support (List.prod []) ≤ List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support [])
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g hd : Perm α
tl : List (Perm α)
hl : support (List.prod tl) ≤ List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support tl)
⊢ support (List.prod (hd :: tl)) ≤ List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support (hd :: tl))
[PROOFSTEP]
rw [List.prod_cons, List.map_cons, List.foldr_cons]
[GOAL]
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g hd : Perm α
tl : List (Perm α)
hl : support (List.prod tl) ≤ List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support tl)
⊢ support (hd * List.prod tl) ≤ support hd ⊔ List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support tl)
[PROOFSTEP]
refine' (support_mul_le hd tl.prod).trans _
[GOAL]
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g hd : Perm α
tl : List (Perm α)
hl : support (List.prod tl) ≤ List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support tl)
⊢ support hd ⊔ support (List.prod tl) ≤ support hd ⊔ List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support tl)
[PROOFSTEP]
exact sup_le_sup le_rfl hl
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : x ≠ y
⊢ support (swap x y) = {x, y}
[PROOFSTEP]
ext z
[GOAL]
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : x ≠ y
z : α
⊢ z ∈ support (swap x y) ↔ z ∈ {x, y}
[PROOFSTEP]
by_cases hx : z = x
[GOAL]
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : x ≠ y
z : α
hx : z = x
⊢ z ∈ support (swap x y) ↔ z ∈ {x, y}
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : x ≠ y
z : α
hx : ¬z = x
⊢ z ∈ support (swap x y) ↔ z ∈ {x, y}
[PROOFSTEP]
any_goals simpa [hx] using h.symm
[GOAL]
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : x ≠ y
z : α
hx : z = x
⊢ z ∈ support (swap x y) ↔ z ∈ {x, y}
[PROOFSTEP]
simpa [hx] using h.symm
[GOAL]
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : x ≠ y
z : α
hx : ¬z = x
⊢ z ∈ support (swap x y) ↔ z ∈ {x, y}
[PROOFSTEP]
simpa [hx] using h.symm
[GOAL]
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : x ≠ y
z : α
hx : ¬z = x
⊢ z ∈ support (swap x y) ↔ z ∈ {x, y}
[PROOFSTEP]
by_cases hy : z = y
[GOAL]
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : x ≠ y
z : α
hx : ¬z = x
hy : z = y
⊢ z ∈ support (swap x y) ↔ z ∈ {x, y}
[PROOFSTEP]
simp [swap_apply_of_ne_of_ne, hx, hy]
[GOAL]
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : x ≠ y
z : α
hx : ¬z = x
hy : z = y
⊢ ¬x = y
[PROOFSTEP]
exact h
[GOAL]
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : x ≠ y
z : α
hx : ¬z = x
hy : ¬z = y
⊢ z ∈ support (swap x y) ↔ z ∈ {x, y}
[PROOFSTEP]
simp [swap_apply_of_ne_of_ne, hx, hy]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
⊢ support (swap x y) = {x, y} ↔ x ≠ y
[PROOFSTEP]
refine' ⟨fun h => _, fun h => support_swap h⟩
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : support (swap x y) = {x, y}
⊢ x ≠ y
[PROOFSTEP]
by_contra'
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : support (swap x y) = {x, y}
this : x = y
⊢ False
[PROOFSTEP]
rw [← this] at h
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : support (swap x x) = {x, x}
this : x = y
⊢ False
[PROOFSTEP]
simp only [swap_self, support_refl, pair_eq_singleton] at h
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
this : x = y
h : ∅ = {x}
⊢ False
[PROOFSTEP]
have : x ∈ ∅ := by
  rw [h]
  exact mem_singleton.mpr rfl
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
this : x = y
h : ∅ = {x}
⊢ x ∈ ∅
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
this : x = y
h : ∅ = {x}
⊢ x ∈ {x}
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
this : x = y
h : ∅ = {x}
⊢ Membership α (Finset α)
[PROOFSTEP]
exact mem_singleton.mpr rfl
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
this✝ : x = y
h : ∅ = {x}
this : x ∈ ∅
⊢ False
[PROOFSTEP]
have := (Finset.ne_empty_of_mem this)
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
this✝¹ : x = y
h : ∅ = {x}
this✝ : x ∈ ∅
this : ∅ ≠ ∅
⊢ False
[PROOFSTEP]
exact this rfl
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y z : α
h : List.Nodup [x, y, z]
⊢ support (swap x y * swap y z) = {x, y, z}
[PROOFSTEP]
simp only [List.not_mem_nil, and_true_iff, List.mem_cons, not_false_iff, List.nodup_cons, List.mem_singleton,
  and_self_iff, List.nodup_nil] at h
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y z : α
h : ¬(x = y ∨ x = z ∨ False) ∧ ¬(y = z ∨ False)
⊢ support (swap x y * swap y z) = {x, y, z}
[PROOFSTEP]
push_neg at h
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
⊢ support (swap x y * swap y z) = {x, y, z}
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
⊢ support (swap x y * swap y z) ≤ {x, y, z}
[PROOFSTEP]
convert support_mul_le (swap x y) (swap y z) using 1
[GOAL]
case h.e'_4
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
⊢ {x, y, z} = support (swap x y) ⊔ support (swap y z)
[PROOFSTEP]
rw [support_swap h.left.left, support_swap h.right.left]
[GOAL]
case h.e'_4
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
⊢ {x, y, z} = {x, y} ⊔ {y, z}
[PROOFSTEP]
simp only [sup_eq_union]
[GOAL]
case h.e'_4
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
⊢ {x, y, z} = {x, y} ∪ {y, z}
[PROOFSTEP]
simp only [mem_singleton, mem_insert, union_insert, insert_union, mem_union, true_or, or_true, insert_eq_of_mem]
[GOAL]
case h.e'_4
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
⊢ {x, y, z} = insert x ({y} ∪ {z})
[PROOFSTEP]
rfl
[GOAL]
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
⊢ {x, y, z} ≤ support (swap x y * swap y z)
[PROOFSTEP]
intro
[GOAL]
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
a✝ : α
⊢ a✝ ∈ {x, y, z} → a✝ ∈ support (swap x y * swap y z)
[PROOFSTEP]
simp only [mem_insert, mem_singleton]
[GOAL]
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
a✝ : α
⊢ a✝ = x ∨ a✝ = y ∨ a✝ = z → a✝ ∈ support (swap x y * swap y z)
[PROOFSTEP]
rintro (rfl | rfl | rfl | _)
[GOAL]
case a.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
y z a✝ : α
h : (a✝ ≠ y ∧ a✝ ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
⊢ a✝ ∈ support (swap a✝ y * swap y z)
[PROOFSTEP]
simp [swap_apply_of_ne_of_ne, h.left.left, h.left.left.symm, h.left.right.symm, h.left.right.left.symm,
  h.right.left.symm]
[GOAL]
case a.inr.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x z a✝ : α
h : (x ≠ a✝ ∧ x ≠ z ∧ ¬False) ∧ a✝ ≠ z ∧ ¬False
⊢ a✝ ∈ support (swap x a✝ * swap a✝ z)
[PROOFSTEP]
simp [swap_apply_of_ne_of_ne, h.left.left, h.left.left.symm, h.left.right.symm, h.left.right.left.symm,
  h.right.left.symm]
[GOAL]
case a.inr.inr.refl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
⊢ z ∈ support (swap x y * swap y z)
[PROOFSTEP]
simp [swap_apply_of_ne_of_ne, h.left.left, h.left.left.symm, h.left.right.symm, h.left.right.left.symm,
  h.right.left.symm]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x y : α
⊢ support f \ {x, y} ≤ support (swap x y * f)
[PROOFSTEP]
intro
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x y a✝ : α
⊢ a✝ ∈ support f \ {x, y} → a✝ ∈ support (swap x y * f)
[PROOFSTEP]
simp only [and_imp, Perm.coe_mul, Function.comp_apply, Ne.def, mem_support, mem_insert, mem_sdiff, mem_singleton]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x y a✝ : α
⊢ ¬↑f a✝ = a✝ → ¬(a✝ = x ∨ a✝ = y) → ¬↑(swap x y) (↑f a✝) = a✝
[PROOFSTEP]
push_neg
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x y a✝ : α
⊢ ↑f a✝ ≠ a✝ → a✝ ≠ x ∧ a✝ ≠ y → ↑(swap x y) (↑f a✝) ≠ a✝
[PROOFSTEP]
rintro ha ⟨hx, hy⟩ H
[GOAL]
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x y a✝ : α
ha : ↑f a✝ ≠ a✝
hx : a✝ ≠ x
hy : a✝ ≠ y
H : ↑(swap x y) (↑f a✝) = a✝
⊢ False
[PROOFSTEP]
rw [swap_apply_eq_iff, swap_apply_of_ne_of_ne hx hy] at H
[GOAL]
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x y a✝ : α
ha : ↑f a✝ ≠ a✝
hx : a✝ ≠ x
hy : a✝ ≠ y
H : ↑f a✝ = a✝
⊢ False
[PROOFSTEP]
exact ha H
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x : α
h : ↑f (↑f x) ≠ x
⊢ support (swap x (↑f x) * f) = support f \ {x}
[PROOFSTEP]
by_cases hx : f x = x
[GOAL]
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x : α
h : ↑f (↑f x) ≠ x
hx : ↑f x = x
⊢ support (swap x (↑f x) * f) = support f \ {x}
[PROOFSTEP]
simp [hx, sdiff_singleton_eq_erase, not_mem_support.mpr hx, erase_eq_of_not_mem]
[GOAL]
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x : α
h : ↑f (↑f x) ≠ x
hx : ¬↑f x = x
⊢ support (swap x (↑f x) * f) = support f \ {x}
[PROOFSTEP]
ext z
[GOAL]
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x : α
h : ↑f (↑f x) ≠ x
hx : ¬↑f x = x
z : α
⊢ z ∈ support (swap x (↑f x) * f) ↔ z ∈ support f \ {x}
[PROOFSTEP]
by_cases hzx : z = x
[GOAL]
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x : α
h : ↑f (↑f x) ≠ x
hx : ¬↑f x = x
z : α
hzx : z = x
⊢ z ∈ support (swap x (↑f x) * f) ↔ z ∈ support f \ {x}
[PROOFSTEP]
simp [hzx]
[GOAL]
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x : α
h : ↑f (↑f x) ≠ x
hx : ¬↑f x = x
z : α
hzx : ¬z = x
⊢ z ∈ support (swap x (↑f x) * f) ↔ z ∈ support f \ {x}
[PROOFSTEP]
by_cases hzf : z = f x
[GOAL]
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x : α
h : ↑f (↑f x) ≠ x
hx : ¬↑f x = x
z : α
hzx : ¬z = x
hzf : z = ↑f x
⊢ z ∈ support (swap x (↑f x) * f) ↔ z ∈ support f \ {x}
[PROOFSTEP]
simp [hzf, hx, h, swap_apply_of_ne_of_ne]
[GOAL]
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x : α
h : ↑f (↑f x) ≠ x
hx : ¬↑f x = x
z : α
hzx : ¬z = x
hzf : ¬z = ↑f x
⊢ z ∈ support (swap x (↑f x) * f) ↔ z ∈ support f \ {x}
[PROOFSTEP]
by_cases hzfx : f z = x
[GOAL]
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x : α
h : ↑f (↑f x) ≠ x
hx : ¬↑f x = x
z : α
hzx : ¬z = x
hzf : ¬z = ↑f x
hzfx : ↑f z = x
⊢ z ∈ support (swap x (↑f x) * f) ↔ z ∈ support f \ {x}
[PROOFSTEP]
simp [Ne.symm hzx, hzx, Ne.symm hzf, hzfx]
[GOAL]
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x : α
h : ↑f (↑f x) ≠ x
hx : ¬↑f x = x
z : α
hzx : ¬z = x
hzf : ¬z = ↑f x
hzfx : ¬↑f z = x
⊢ z ∈ support (swap x (↑f x) * f) ↔ z ∈ support f \ {x}
[PROOFSTEP]
simp [Ne.symm hzx, hzx, Ne.symm hzf, hzfx, f.injective.ne hzx, swap_apply_of_ne_of_ne]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hy : y ∈ support (swap x (↑f x) * f)
⊢ y ∈ support f ∧ y ≠ x
[PROOFSTEP]
simp only [mem_support, swap_apply_def, mul_apply, f.injective.eq_iff] at *
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hy : (if ↑f y = x then ↑f x else if y = x then x else ↑f y) ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
by_cases h : f y = x
[GOAL]
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hy : (if ↑f y = x then ↑f x else if y = x then x else ↑f y) ≠ y
h : ↑f y = x
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
constructor
[GOAL]
case pos.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hy : (if ↑f y = x then ↑f x else if y = x then x else ↑f y) ≠ y
h : ↑f y = x
⊢ ↑f y ≠ y
[PROOFSTEP]
intro
[GOAL]
case pos.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hy : (if ↑f y = x then ↑f x else if y = x then x else ↑f y) ≠ y
h : ↑f y = x
⊢ y ≠ x
[PROOFSTEP]
intro
[GOAL]
case pos.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hy : (if ↑f y = x then ↑f x else if y = x then x else ↑f y) ≠ y
h : ↑f y = x
a✝ : ↑f y = y
⊢ False
[PROOFSTEP]
simp_all only [if_true, eq_self_iff_true, not_true, Ne.def]
[GOAL]
case pos.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hy : (if ↑f y = x then ↑f x else if y = x then x else ↑f y) ≠ y
h : ↑f y = x
a✝ : y = x
⊢ False
[PROOFSTEP]
simp_all only [if_true, eq_self_iff_true, not_true, Ne.def]
[GOAL]
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hy : (if ↑f y = x then ↑f x else if y = x then x else ↑f y) ≠ y
h : ¬↑f y = x
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
split_ifs at hy  with hf heq
[GOAL]
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : ¬↑f y = x
hf : ↑f y = x
hy : ↑f x ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
simp_all only [not_true]
[GOAL]
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : ¬↑f y = x
hf : ¬↑f y = x
heq : y = x
hy : x ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
simp_all only [not_true]
[GOAL]
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : ¬↑f y = x
hf : ¬↑f y = x
heq : ¬y = x
hy : ↑f y ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
simp_all only [not_true]
[GOAL]
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : ¬↑f x = x
heq : y = x
hy : x ≠ x
⊢ ↑f x ≠ x ∧ x ≠ x
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hf : ¬↑f y = x
heq : ¬y = x
hy : ↑f y ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
exact ⟨h, hy⟩
[GOAL]
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hf : ¬↑f y = x
heq : ¬y = x
hy : ↑f y ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
refine' ⟨hy, heq⟩
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h : f ∈ l
hl : List.Pairwise Disjoint l
⊢ ∀ (x : α), x ∈ support f → ↑f x = ↑(List.prod l) x
[PROOFSTEP]
induction' l with hd tl IH
[GOAL]
case nil
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : f ∈ l
hl✝ : List.Pairwise Disjoint l
h : f ∈ []
hl : List.Pairwise Disjoint []
⊢ ∀ (x : α), x ∈ support f → ↑f x = ↑(List.prod []) x
[PROOFSTEP]
simp at h
[GOAL]
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : f ∈ l
hl✝ : List.Pairwise Disjoint l
hd : Perm α
tl : List (Perm α)
IH : f ∈ tl → List.Pairwise Disjoint tl → ∀ (x : α), x ∈ support f → ↑f x = ↑(List.prod tl) x
h : f ∈ hd :: tl
hl : List.Pairwise Disjoint (hd :: tl)
⊢ ∀ (x : α), x ∈ support f → ↑f x = ↑(List.prod (hd :: tl)) x
[PROOFSTEP]
intro x hx
[GOAL]
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : f ∈ l
hl✝ : List.Pairwise Disjoint l
hd : Perm α
tl : List (Perm α)
IH : f ∈ tl → List.Pairwise Disjoint tl → ∀ (x : α), x ∈ support f → ↑f x = ↑(List.prod tl) x
h : f ∈ hd :: tl
hl : List.Pairwise Disjoint (hd :: tl)
x : α
hx : x ∈ support f
⊢ ↑f x = ↑(List.prod (hd :: tl)) x
[PROOFSTEP]
rw [List.pairwise_cons] at hl
[GOAL]
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : f ∈ l
hl✝ : List.Pairwise Disjoint l
hd : Perm α
tl : List (Perm α)
IH : f ∈ tl → List.Pairwise Disjoint tl → ∀ (x : α), x ∈ support f → ↑f x = ↑(List.prod tl) x
h : f ∈ hd :: tl
hl : (∀ (a' : Perm α), a' ∈ tl → Disjoint hd a') ∧ List.Pairwise Disjoint tl
x : α
hx : x ∈ support f
⊢ ↑f x = ↑(List.prod (hd :: tl)) x
[PROOFSTEP]
rw [List.mem_cons] at h
[GOAL]
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : f ∈ l
hl✝ : List.Pairwise Disjoint l
hd : Perm α
tl : List (Perm α)
IH : f ∈ tl → List.Pairwise Disjoint tl → ∀ (x : α), x ∈ support f → ↑f x = ↑(List.prod tl) x
h : f = hd ∨ f ∈ tl
hl : (∀ (a' : Perm α), a' ∈ tl → Disjoint hd a') ∧ List.Pairwise Disjoint tl
x : α
hx : x ∈ support f
⊢ ↑f x = ↑(List.prod (hd :: tl)) x
[PROOFSTEP]
rcases h with (rfl | h)
[GOAL]
case cons.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h : f ∈ l
hl✝ : List.Pairwise Disjoint l
tl : List (Perm α)
IH : f ∈ tl → List.Pairwise Disjoint tl → ∀ (x : α), x ∈ support f → ↑f x = ↑(List.prod tl) x
x : α
hx : x ∈ support f
hl : (∀ (a' : Perm α), a' ∈ tl → Disjoint f a') ∧ List.Pairwise Disjoint tl
⊢ ↑f x = ↑(List.prod (f :: tl)) x
[PROOFSTEP]
rw [List.prod_cons, mul_apply, not_mem_support.mp ((disjoint_prod_right tl hl.left).mem_imp hx)]
[GOAL]
case cons.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : f ∈ l
hl✝ : List.Pairwise Disjoint l
hd : Perm α
tl : List (Perm α)
IH : f ∈ tl → List.Pairwise Disjoint tl → ∀ (x : α), x ∈ support f → ↑f x = ↑(List.prod tl) x
hl : (∀ (a' : Perm α), a' ∈ tl → Disjoint hd a') ∧ List.Pairwise Disjoint tl
x : α
hx : x ∈ support f
h : f ∈ tl
⊢ ↑f x = ↑(List.prod (hd :: tl)) x
[PROOFSTEP]
rw [List.prod_cons, mul_apply, ← IH h hl.right _ hx, eq_comm, ← not_mem_support]
[GOAL]
case cons.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : f ∈ l
hl✝ : List.Pairwise Disjoint l
hd : Perm α
tl : List (Perm α)
IH : f ∈ tl → List.Pairwise Disjoint tl → ∀ (x : α), x ∈ support f → ↑f x = ↑(List.prod tl) x
hl : (∀ (a' : Perm α), a' ∈ tl → Disjoint hd a') ∧ List.Pairwise Disjoint tl
x : α
hx : x ∈ support f
h : f ∈ tl
⊢ ¬↑f x ∈ support hd
[PROOFSTEP]
refine' (hl.left _ h).symm.mem_imp _
[GOAL]
case cons.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : f ∈ l
hl✝ : List.Pairwise Disjoint l
hd : Perm α
tl : List (Perm α)
IH : f ∈ tl → List.Pairwise Disjoint tl → ∀ (x : α), x ∈ support f → ↑f x = ↑(List.prod tl) x
hl : (∀ (a' : Perm α), a' ∈ tl → Disjoint hd a') ∧ List.Pairwise Disjoint tl
x : α
hx : x ∈ support f
h : f ∈ tl
⊢ ↑f x ∈ support f
[PROOFSTEP]
simpa using hx
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g x y : Perm α
h : Disjoint f g
hf : support x ≤ support f
hg : support y ≤ support g
⊢ Disjoint x y
[PROOFSTEP]
rw [disjoint_iff_disjoint_support] at h ⊢
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g x y : Perm α
h✝ : Disjoint f g
h : _root_.Disjoint (support f) (support g)
hf : support x ≤ support f
hg : support y ≤ support g
⊢ _root_.Disjoint (support x) (support y)
[PROOFSTEP]
exact h.mono hf hg
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h : f ∈ l
hl : List.Pairwise Disjoint l
⊢ support f ≤ support (List.prod l)
[PROOFSTEP]
intro x hx
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h : f ∈ l
hl : List.Pairwise Disjoint l
x : α
hx : x ∈ support f
⊢ x ∈ support (List.prod l)
[PROOFSTEP]
rwa [mem_support, ← eq_on_support_mem_disjoint h hl _ hx, ← mem_support]
[GOAL]
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
f✝ g✝ : Perm α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
⊢ support (extendDomain g f) = map (asEmbedding f) (support g)
[PROOFSTEP]
ext b
[GOAL]
case a
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
f✝ g✝ : Perm α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
⊢ b ∈ support (extendDomain g f) ↔ b ∈ map (asEmbedding f) (support g)
[PROOFSTEP]
simp only [exists_prop, Function.Embedding.coeFn_mk, toEmbedding_apply, mem_map, Ne.def, Function.Embedding.trans_apply,
  mem_support]
[GOAL]
case a
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
f✝ g✝ : Perm α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
⊢ ¬↑(extendDomain g f) b = b ↔ ∃ a, ¬↑g a = a ∧ ↑(asEmbedding f) a = b
[PROOFSTEP]
by_cases pb : p b
[GOAL]
case pos
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
f✝ g✝ : Perm α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : p b
⊢ ¬↑(extendDomain g f) b = b ↔ ∃ a, ¬↑g a = a ∧ ↑(asEmbedding f) a = b
[PROOFSTEP]
rw [extendDomain_apply_subtype _ _ pb]
[GOAL]
case pos
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
f✝ g✝ : Perm α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : p b
⊢ ¬↑(↑f (↑g (↑f.symm { val := b, property := pb }))) = b ↔ ∃ a, ¬↑g a = a ∧ ↑(asEmbedding f) a = b
[PROOFSTEP]
constructor
[GOAL]
case pos.mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
f✝ g✝ : Perm α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : p b
⊢ ¬↑(↑f (↑g (↑f.symm { val := b, property := pb }))) = b → ∃ a, ¬↑g a = a ∧ ↑(asEmbedding f) a = b
[PROOFSTEP]
rintro h
[GOAL]
case pos.mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
f✝ g✝ : Perm α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : p b
h : ¬↑(↑f (↑g (↑f.symm { val := b, property := pb }))) = b
⊢ ∃ a, ¬↑g a = a ∧ ↑(asEmbedding f) a = b
[PROOFSTEP]
refine' ⟨f.symm ⟨b, pb⟩, _, by simp⟩
[GOAL]
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
f✝ g✝ : Perm α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : p b
h : ¬↑(↑f (↑g (↑f.symm { val := b, property := pb }))) = b
⊢ ↑(asEmbedding f) (↑f.symm { val := b, property := pb }) = b
[PROOFSTEP]
simp
[GOAL]
case pos.mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
f✝ g✝ : Perm α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : p b
h : ¬↑(↑f (↑g (↑f.symm { val := b, property := pb }))) = b
⊢ ¬↑g (↑f.symm { val := b, property := pb }) = ↑f.symm { val := b, property := pb }
[PROOFSTEP]
contrapose! h
[GOAL]
case pos.mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
f✝ g✝ : Perm α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : p b
h : ↑g (↑f.symm { val := b, property := pb }) = ↑f.symm { val := b, property := pb }
⊢ ↑(↑f (↑g (↑f.symm { val := b, property := pb }))) = b
[PROOFSTEP]
simp [h]
[GOAL]
case pos.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
f✝ g✝ : Perm α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : p b
⊢ (∃ a, ¬↑g a = a ∧ ↑(asEmbedding f) a = b) → ¬↑(↑f (↑g (↑f.symm { val := b, property := pb }))) = b
[PROOFSTEP]
rintro ⟨a, ha, hb⟩
[GOAL]
case pos.mpr.intro.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
f✝ g✝ : Perm α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : p b
a : α
ha : ¬↑g a = a
hb : ↑(asEmbedding f) a = b
⊢ ¬↑(↑f (↑g (↑f.symm { val := b, property := pb }))) = b
[PROOFSTEP]
contrapose! ha
[GOAL]
case pos.mpr.intro.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
f✝ g✝ : Perm α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : p b
a : α
hb : ↑(asEmbedding f) a = b
ha : ↑(↑f (↑g (↑f.symm { val := b, property := pb }))) = b
⊢ ↑g a = a
[PROOFSTEP]
obtain rfl : a = f.symm ⟨b, pb⟩ := by
  rw [eq_symm_apply]
  exact Subtype.coe_injective hb
[GOAL]
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
f✝ g✝ : Perm α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : p b
a : α
hb : ↑(asEmbedding f) a = b
ha : ↑(↑f (↑g (↑f.symm { val := b, property := pb }))) = b
⊢ a = ↑f.symm { val := b, property := pb }
[PROOFSTEP]
rw [eq_symm_apply]
[GOAL]
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
f✝ g✝ : Perm α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : p b
a : α
hb : ↑(asEmbedding f) a = b
ha : ↑(↑f (↑g (↑f.symm { val := b, property := pb }))) = b
⊢ ↑f a = { val := b, property := pb }
[PROOFSTEP]
exact Subtype.coe_injective hb
[GOAL]
case pos.mpr.intro.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
f✝ g✝ : Perm α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : p b
ha : ↑(↑f (↑g (↑f.symm { val := b, property := pb }))) = b
hb : ↑(asEmbedding f) (↑f.symm { val := b, property := pb }) = b
⊢ ↑g (↑f.symm { val := b, property := pb }) = ↑f.symm { val := b, property := pb }
[PROOFSTEP]
rw [eq_symm_apply]
[GOAL]
case pos.mpr.intro.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
f✝ g✝ : Perm α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : p b
ha : ↑(↑f (↑g (↑f.symm { val := b, property := pb }))) = b
hb : ↑(asEmbedding f) (↑f.symm { val := b, property := pb }) = b
⊢ ↑f (↑g (↑f.symm { val := b, property := pb })) = { val := b, property := pb }
[PROOFSTEP]
exact Subtype.coe_injective ha
[GOAL]
case neg
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
f✝ g✝ : Perm α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : ¬p b
⊢ ¬↑(extendDomain g f) b = b ↔ ∃ a, ¬↑g a = a ∧ ↑(asEmbedding f) a = b
[PROOFSTEP]
rw [extendDomain_apply_not_subtype _ _ pb]
[GOAL]
case neg
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
f✝ g✝ : Perm α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : ¬p b
⊢ ¬b = b ↔ ∃ a, ¬↑g a = a ∧ ↑(asEmbedding f) a = b
[PROOFSTEP]
simp only [not_exists, false_iff_iff, not_and, eq_self_iff_true, not_true]
[GOAL]
case neg
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
f✝ g✝ : Perm α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : ¬p b
⊢ ∀ (x : α), ¬↑g x = x → ¬↑(asEmbedding f) x = b
[PROOFSTEP]
rintro a _ rfl
[GOAL]
case neg
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
f✝ g✝ : Perm α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
a : α
a✝ : ¬↑g a = a
pb : ¬p (↑(asEmbedding f) a)
⊢ False
[PROOFSTEP]
exact pb (Subtype.prop _)
[GOAL]
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
f✝ g✝ : Perm α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
⊢ card (support (extendDomain g f)) = card (support g)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
⊢ card (support f) = 0 ↔ f = 1
[PROOFSTEP]
rw [Finset.card_eq_zero, support_eq_empty_iff]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : f ≠ 1
⊢ 1 < card (support f)
[PROOFSTEP]
simp_rw [one_lt_card_iff, mem_support, ← not_or]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : f ≠ 1
⊢ ∃ a b, ¬(↑f a = a ∨ ↑f b = b ∨ a = b)
[PROOFSTEP]
contrapose! h
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : ∀ (a b : α), ↑f a = a ∨ ↑f b = b ∨ a = b
⊢ f = 1
[PROOFSTEP]
ext a
[GOAL]
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : ∀ (a b : α), ↑f a = a ∨ ↑f b = b ∨ a = b
a : α
⊢ ↑f a = ↑1 a
[PROOFSTEP]
specialize h (f a) a
[GOAL]
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
a : α
h : ↑f (↑f a) = ↑f a ∨ ↑f a = a ∨ ↑f a = a
⊢ ↑f a = ↑1 a
[PROOFSTEP]
rwa [apply_eq_iff_eq, or_self_iff, or_self_iff] at h
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
⊢ card (support f) ≠ 1
[PROOFSTEP]
by_cases h : f = 1
[GOAL]
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : f = 1
⊢ card (support f) ≠ 1
[PROOFSTEP]
exact ne_of_eq_of_ne (card_support_eq_zero.mpr h) zero_ne_one
[GOAL]
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : ¬f = 1
⊢ card (support f) ≠ 1
[PROOFSTEP]
exact ne_of_gt (one_lt_card_support_of_ne_one h)
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
⊢ card (support f) ≤ 1 ↔ f = 1
[PROOFSTEP]
rw [le_iff_lt_or_eq, Nat.lt_succ_iff, le_zero_iff, card_support_eq_zero, or_iff_not_imp_right,
  imp_iff_right f.card_support_ne_one]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x : α
hx : ↑f x ≠ x
h : support f ⊆ support (swap x (↑f x) * f)
⊢ ¬↑(swap x (↑f x) * f) x ≠ x
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hxy : x ≠ y
⊢ Multiset.Nodup (x ::ₘ y ::ₘ 0)
[PROOFSTEP]
simp [hxy]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hxy : x ≠ y
⊢ support (swap x y) = { val := x ::ₘ y ::ₘ 0, nodup := (_ : Multiset.Nodup (x ::ₘ {y})) }
[PROOFSTEP]
simp [support_swap hxy, *, Finset.ext_iff]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
⊢ card (support f) = 2 ↔ IsSwap f
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
⊢ card (support f) = 2 → IsSwap f
[PROOFSTEP]
intro h
[GOAL]
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
⊢ IsSwap f → card (support f) = 2
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : card (support f) = 2
⊢ IsSwap f
[PROOFSTEP]
obtain ⟨x, t, hmem, hins, ht⟩ := card_eq_succ.1 h
[GOAL]
case mp.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : card (support f) = 2
x : α
t : Finset α
hmem : ¬x ∈ t
hins : insert x t = support f
ht : card t = 1
⊢ IsSwap f
[PROOFSTEP]
obtain ⟨y, rfl⟩ := card_eq_one.1 ht
[GOAL]
case mp.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : card (support f) = 2
x y : α
hmem : ¬x ∈ {y}
hins : {x, y} = support f
ht : card {y} = 1
⊢ IsSwap f
[PROOFSTEP]
rw [mem_singleton] at hmem
[GOAL]
case mp.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : card (support f) = 2
x y : α
hmem : ¬x = y
hins : {x, y} = support f
ht : card {y} = 1
⊢ IsSwap f
[PROOFSTEP]
refine' ⟨x, y, hmem, _⟩
[GOAL]
case mp.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : card (support f) = 2
x y : α
hmem : ¬x = y
hins : {x, y} = support f
ht : card {y} = 1
⊢ f = swap x y
[PROOFSTEP]
ext a
[GOAL]
case mp.intro.intro.intro.intro.intro.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : card (support f) = 2
x y : α
hmem : ¬x = y
hins : {x, y} = support f
ht : card {y} = 1
a : α
⊢ ↑f a = ↑(swap x y) a
[PROOFSTEP]
have key : ∀ b, f b ≠ b ↔ _ := fun b => by rw [← mem_support, ← hins, mem_insert, mem_singleton]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : card (support f) = 2
x y : α
hmem : ¬x = y
hins : {x, y} = support f
ht : card {y} = 1
a b : α
⊢ ↑f b ≠ b ↔ ?m.195733 b
[PROOFSTEP]
rw [← mem_support, ← hins, mem_insert, mem_singleton]
[GOAL]
case mp.intro.intro.intro.intro.intro.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : card (support f) = 2
x y : α
hmem : ¬x = y
hins : {x, y} = support f
ht : card {y} = 1
a : α
key : ∀ (b : α), ↑f b ≠ b ↔ b = x ∨ b = y
⊢ ↑f a = ↑(swap x y) a
[PROOFSTEP]
by_cases ha : f a = a
[GOAL]
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : card (support f) = 2
x y : α
hmem : ¬x = y
hins : {x, y} = support f
ht : card {y} = 1
a : α
key : ∀ (b : α), ↑f b ≠ b ↔ b = x ∨ b = y
ha : ↑f a = a
⊢ ↑f a = ↑(swap x y) a
[PROOFSTEP]
have ha' := not_or.mp (mt (key a).mpr (not_not.mpr ha))
[GOAL]
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : card (support f) = 2
x y : α
hmem : ¬x = y
hins : {x, y} = support f
ht : card {y} = 1
a : α
key : ∀ (b : α), ↑f b ≠ b ↔ b = x ∨ b = y
ha : ↑f a = a
ha' : ¬a = x ∧ ¬a = y
⊢ ↑f a = ↑(swap x y) a
[PROOFSTEP]
rw [ha, swap_apply_of_ne_of_ne ha'.1 ha'.2]
[GOAL]
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : card (support f) = 2
x y : α
hmem : ¬x = y
hins : {x, y} = support f
ht : card {y} = 1
a : α
key : ∀ (b : α), ↑f b ≠ b ↔ b = x ∨ b = y
ha : ¬↑f a = a
⊢ ↑f a = ↑(swap x y) a
[PROOFSTEP]
have ha' := (key (f a)).mp (mt f.apply_eq_iff_eq.mp ha)
[GOAL]
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : card (support f) = 2
x y : α
hmem : ¬x = y
hins : {x, y} = support f
ht : card {y} = 1
a : α
key : ∀ (b : α), ↑f b ≠ b ↔ b = x ∨ b = y
ha : ¬↑f a = a
ha' : ↑f a = x ∨ ↑f a = y
⊢ ↑f a = ↑(swap x y) a
[PROOFSTEP]
obtain rfl | rfl := (key a).mp ha
[GOAL]
case neg.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : card (support f) = 2
y : α
ht : card {y} = 1
a : α
ha : ¬↑f a = a
hmem : ¬a = y
hins : {a, y} = support f
key : ∀ (b : α), ↑f b ≠ b ↔ b = a ∨ b = y
ha' : ↑f a = a ∨ ↑f a = y
⊢ ↑f a = ↑(swap a y) a
[PROOFSTEP]
rw [Or.resolve_left ha' ha, swap_apply_left]
[GOAL]
case neg.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : card (support f) = 2
x a : α
ha : ¬↑f a = a
hmem : ¬x = a
hins : {x, a} = support f
ht : card {a} = 1
key : ∀ (b : α), ↑f b ≠ b ↔ b = x ∨ b = a
ha' : ↑f a = x ∨ ↑f a = a
⊢ ↑f a = ↑(swap x a) a
[PROOFSTEP]
rw [Or.resolve_right ha' ha, swap_apply_right]
[GOAL]
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : IsSwap f
⊢ card (support f) = 2
[PROOFSTEP]
obtain ⟨x, y, hxy, rfl⟩ := h
[GOAL]
case mpr.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hxy : x ≠ y
⊢ card (support (swap x y)) = 2
[PROOFSTEP]
exact card_support_swap hxy
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : Disjoint f g
⊢ card (support (f * g)) = card (support f) + card (support g)
[PROOFSTEP]
rw [← Finset.card_disjoint_union]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : Disjoint f g
⊢ card (support (f * g)) = card (support f ∪ support g)
[PROOFSTEP]
congr
[GOAL]
case e_s
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : Disjoint f g
⊢ support (f * g) = support f ∪ support g
[PROOFSTEP]
ext
[GOAL]
case e_s.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : Disjoint f g
a✝ : α
⊢ a✝ ∈ support (f * g) ↔ a✝ ∈ support f ∪ support g
[PROOFSTEP]
simp [h.support_mul]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : Disjoint f g
⊢ _root_.Disjoint (support f) (support g)
[PROOFSTEP]
simpa using h.disjoint_support
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h : List.Pairwise Disjoint l
⊢ card (support (List.prod l)) = List.sum (List.map (card ∘ support) l)
[PROOFSTEP]
induction' l with a t ih
[GOAL]
case nil
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : List.Pairwise Disjoint l
h : List.Pairwise Disjoint []
⊢ card (support (List.prod [])) = List.sum (List.map (card ∘ support) [])
[PROOFSTEP]
exact card_support_eq_zero.mpr rfl
[GOAL]
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : List.Pairwise Disjoint l
a : Perm α
t : List (Perm α)
ih : List.Pairwise Disjoint t → card (support (List.prod t)) = List.sum (List.map (card ∘ support) t)
h : List.Pairwise Disjoint (a :: t)
⊢ card (support (List.prod (a :: t))) = List.sum (List.map (card ∘ support) (a :: t))
[PROOFSTEP]
obtain ⟨ha, ht⟩ := List.pairwise_cons.1 h
[GOAL]
case cons.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : List.Pairwise Disjoint l
a : Perm α
t : List (Perm α)
ih : List.Pairwise Disjoint t → card (support (List.prod t)) = List.sum (List.map (card ∘ support) t)
h : List.Pairwise Disjoint (a :: t)
ha : ∀ (a' : Perm α), a' ∈ t → Disjoint a a'
ht : List.Pairwise Disjoint t
⊢ card (support (List.prod (a :: t))) = List.sum (List.map (card ∘ support) (a :: t))
[PROOFSTEP]
rw [List.prod_cons, List.map_cons, List.sum_cons, ← ih ht]
[GOAL]
case cons.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : List.Pairwise Disjoint l
a : Perm α
t : List (Perm α)
ih : List.Pairwise Disjoint t → card (support (List.prod t)) = List.sum (List.map (card ∘ support) t)
h : List.Pairwise Disjoint (a :: t)
ha : ∀ (a' : Perm α), a' ∈ t → Disjoint a a'
ht : List.Pairwise Disjoint t
⊢ card (support (a * List.prod t)) = (card ∘ support) a + card (support (List.prod t))
[PROOFSTEP]
exact (disjoint_prod_right _ ha).card_support_mul
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
f : Perm α
h : ∀ (x : α), x ∈ s ↔ ↑f x ∈ s
⊢ support (subtypePerm f h) = filter (fun x => decide (↑f ↑x ≠ ↑x) = true) (attach s)
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
f : Perm α
h : ∀ (x : α), x ∈ s ↔ ↑f x ∈ s
a✝ : { x // x ∈ s }
⊢ a✝ ∈ support (subtypePerm f h) ↔ a✝ ∈ filter (fun x => decide (↑f ↑x ≠ ↑x) = true) (attach s)
[PROOFSTEP]
simp [Subtype.ext_iff]


[GOAL]
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ Saturated H ↔ ∀ (n : ℤ) (g : G), g ^ n ∈ H → n = 0 ∨ g ∈ H
[PROOFSTEP]
constructor
[GOAL]
case mp
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ Saturated H → ∀ (n : ℤ) (g : G), g ^ n ∈ H → n = 0 ∨ g ∈ H
[PROOFSTEP]
intros hH n g hgn
[GOAL]
case mp
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : Saturated H
n : ℤ
g : G
hgn : g ^ n ∈ H
⊢ n = 0 ∨ g ∈ H
[PROOFSTEP]
induction' n with n n
[GOAL]
case mp.ofNat
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : Saturated H
n✝ : ℤ
g : G
hgn✝ : g ^ n✝ ∈ H
n : ℕ
hgn : g ^ Int.ofNat n ∈ H
⊢ Int.ofNat n = 0 ∨ g ∈ H
[PROOFSTEP]
simp only [Int.coe_nat_eq_zero, Int.ofNat_eq_coe, zpow_ofNat] at hgn ⊢
[GOAL]
case mp.ofNat
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : Saturated H
n✝ : ℤ
g : G
hgn✝ : g ^ n✝ ∈ H
n : ℕ
hgn : g ^ n ∈ H
⊢ n = 0 ∨ g ∈ H
[PROOFSTEP]
exact hH hgn
[GOAL]
case mp.negSucc
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : Saturated H
n✝ : ℤ
g : G
hgn✝ : g ^ n✝ ∈ H
n : ℕ
hgn : g ^ Int.negSucc n ∈ H
⊢ Int.negSucc n = 0 ∨ g ∈ H
[PROOFSTEP]
suffices g ^ (n + 1) ∈ H by
  refine' (hH this).imp _ id
  simp only [IsEmpty.forall_iff, Nat.succ_ne_zero]
[GOAL]
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : Saturated H
n✝ : ℤ
g : G
hgn✝ : g ^ n✝ ∈ H
n : ℕ
hgn : g ^ Int.negSucc n ∈ H
this : g ^ (n + 1) ∈ H
⊢ Int.negSucc n = 0 ∨ g ∈ H
[PROOFSTEP]
refine' (hH this).imp _ id
[GOAL]
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : Saturated H
n✝ : ℤ
g : G
hgn✝ : g ^ n✝ ∈ H
n : ℕ
hgn : g ^ Int.negSucc n ∈ H
this : g ^ (n + 1) ∈ H
⊢ n + 1 = 0 → Int.negSucc n = 0
[PROOFSTEP]
simp only [IsEmpty.forall_iff, Nat.succ_ne_zero]
[GOAL]
case mp.negSucc
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : Saturated H
n✝ : ℤ
g : G
hgn✝ : g ^ n✝ ∈ H
n : ℕ
hgn : g ^ Int.negSucc n ∈ H
⊢ g ^ (n + 1) ∈ H
[PROOFSTEP]
simpa only [inv_mem_iff, zpow_negSucc] using hgn
[GOAL]
case mpr
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (∀ (n : ℤ) (g : G), g ^ n ∈ H → n = 0 ∨ g ∈ H) → Saturated H
[PROOFSTEP]
intro h n g hgn
[GOAL]
case mpr
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : ∀ (n : ℤ) (g : G), g ^ n ∈ H → n = 0 ∨ g ∈ H
n : ℕ
g : G
hgn : g ^ n ∈ H
⊢ n = 0 ∨ g ∈ H
[PROOFSTEP]
specialize h n g
[GOAL]
case mpr
G : Type u_1
inst✝ : Group G
H : Subgroup G
n : ℕ
g : G
hgn : g ^ n ∈ H
h : g ^ ↑n ∈ H → ↑n = 0 ∨ g ∈ H
⊢ n = 0 ∨ g ∈ H
[PROOFSTEP]
simp only [Int.coe_nat_eq_zero, zpow_ofNat] at h
[GOAL]
case mpr
G : Type u_1
inst✝ : Group G
H : Subgroup G
n : ℕ
g : G
hgn : g ^ n ∈ H
h : g ^ n ∈ H → n = 0 ∨ g ∈ H
⊢ n = 0 ∨ g ∈ H
[PROOFSTEP]
apply h hgn
[GOAL]
A₁ : Type u_1
A₂ : Type u_2
inst✝² : AddCommGroup A₁
inst✝¹ : AddCommGroup A₂
inst✝ : NoZeroSMulDivisors ℕ A₂
f : A₁ →+ A₂
⊢ Saturated (AddMonoidHom.ker f)
[PROOFSTEP]
intro n g hg
[GOAL]
A₁ : Type u_1
A₂ : Type u_2
inst✝² : AddCommGroup A₁
inst✝¹ : AddCommGroup A₂
inst✝ : NoZeroSMulDivisors ℕ A₂
f : A₁ →+ A₂
n : ℕ
g : A₁
hg : n • g ∈ AddMonoidHom.ker f
⊢ n = 0 ∨ g ∈ AddMonoidHom.ker f
[PROOFSTEP]
simpa only [f.mem_ker, nsmul_eq_smul, f.map_nsmul, smul_eq_zero] using hg


[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S✝ : Subsemigroup M
f : M →ₙ* N
S : Subsemigroup N
a✝ b✝ : M
ha : a✝ ∈ ↑f ⁻¹' ↑S
hb : b✝ ∈ ↑f ⁻¹' ↑S
⊢ ↑f (a✝ * b✝) ∈ S
[PROOFSTEP]
rw [map_mul]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S✝ : Subsemigroup M
f : M →ₙ* N
S : Subsemigroup N
a✝ b✝ : M
ha : a✝ ∈ ↑f ⁻¹' ↑S
hb : b✝ ∈ ↑f ⁻¹' ↑S
⊢ ↑f a✝ * ↑f b✝ ∈ S
[PROOFSTEP]
exact mul_mem ha hb
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S✝ : Subsemigroup M
S : Subsemigroup P
⊢ ∀ (x : P), x ∈ comap (MulHom.id P) S ↔ x ∈ S
[PROOFSTEP]
simp
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S✝ : Subsemigroup M
f : M →ₙ* N
S : Subsemigroup M
⊢ ∀ {a b : N}, a ∈ ↑f '' ↑S → b ∈ ↑f '' ↑S → a * b ∈ ↑f '' ↑S
[PROOFSTEP]
rintro _ _ ⟨x, hx, rfl⟩ ⟨y, hy, rfl⟩
[GOAL]
case intro.intro.intro.intro
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S✝ : Subsemigroup M
f : M →ₙ* N
S : Subsemigroup M
x : M
hx : x ∈ ↑S
y : M
hy : y ∈ ↑S
⊢ ↑f x * ↑f y ∈ ↑f '' ↑S
[PROOFSTEP]
exact ⟨x * y, @mul_mem (Subsemigroup M) M _ _ _ _ _ _ hx hy, by rw [map_mul]⟩
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S✝ : Subsemigroup M
f : M →ₙ* N
S : Subsemigroup M
x : M
hx : x ∈ ↑S
y : M
hy : y ∈ ↑S
⊢ ↑f (x * y) = ↑f x * ↑f y
[PROOFSTEP]
rw [map_mul]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S✝ : Subsemigroup M
ι : Type u_5
f : M →ₙ* N
hf : Function.Injective ↑f
S : Subsemigroup M
x : M
⊢ x ∈ comap f (map f S) → x ∈ S
[PROOFSTEP]
simp [mem_comap, mem_map, hf.eq_iff]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S✝ : Subsemigroup M
ι : Type u_5
f : M →ₙ* N
hf : Function.Surjective ↑f
S : Subsemigroup N
x : N
h : x ∈ S
y : M
hy : ↑f y = x
⊢ y ∈ comap f S ∧ ↑f y = x
[PROOFSTEP]
simp [hy, h]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S : Subsemigroup M
s : Set M
x✝¹ : { x // x ∈ closure s }
x : M
hx : x ∈ closure s
x✝ : { val := x, property := hx } ∈ ⊤
⊢ { val := x, property := hx } ∈ closure (Subtype.val ⁻¹' s)
[PROOFSTEP]
refine' closure_induction' _ (fun g hg => subset_closure hg) (fun g₁ g₂ hg₁ hg₂ => _) hx
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S : Subsemigroup M
s : Set M
x✝¹ : { x // x ∈ closure s }
x : M
hx : x ∈ closure s
x✝ : { val := x, property := hx } ∈ ⊤
g₁ : M
g₂ : g₁ ∈ closure s
hg₁ : M
hg₂ : hg₁ ∈ closure s
⊢ { val := g₁, property := g₂ } ∈ closure (Subtype.val ⁻¹' s) →
    { val := hg₁, property := hg₂ } ∈ closure (Subtype.val ⁻¹' s) →
      { val := g₁ * hg₁, property := (_ : g₁ * hg₁ ∈ closure s) } ∈ closure (Subtype.val ⁻¹' s)
[PROOFSTEP]
exact Subsemigroup.mul_mem _
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S s : Subsemigroup M
x : M × N
⊢ x ∈ prod s ⊤ ↔ x ∈ comap (MulHom.fst M N) s
[PROOFSTEP]
simp [mem_prod, MulHom.coe_fst]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S : Subsemigroup M
s : Subsemigroup N
x : M × N
⊢ x ∈ prod ⊤ s ↔ x ∈ comap (MulHom.snd M N) s
[PROOFSTEP]
simp [mem_prod, MulHom.coe_snd]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S : Subsemigroup M
⊢ ↑(prod ⊥ ⊥) = ↑⊥
[PROOFSTEP]
simp [coe_prod, Prod.one_eq_mk]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S s : Subsemigroup M
t : Subsemigroup N
u : Subsemigroup (M × N)
⊢ u ≤ prod s t ↔ map (fst M N) u ≤ s ∧ map (snd M N) u ≤ t
[PROOFSTEP]
constructor
[GOAL]
case mp
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S s : Subsemigroup M
t : Subsemigroup N
u : Subsemigroup (M × N)
⊢ u ≤ prod s t → map (fst M N) u ≤ s ∧ map (snd M N) u ≤ t
[PROOFSTEP]
intro h
[GOAL]
case mp
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S s : Subsemigroup M
t : Subsemigroup N
u : Subsemigroup (M × N)
h : u ≤ prod s t
⊢ map (fst M N) u ≤ s ∧ map (snd M N) u ≤ t
[PROOFSTEP]
constructor
[GOAL]
case mp.left
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S s : Subsemigroup M
t : Subsemigroup N
u : Subsemigroup (M × N)
h : u ≤ prod s t
⊢ map (fst M N) u ≤ s
[PROOFSTEP]
rintro x ⟨⟨y1, y2⟩, ⟨hy1, rfl⟩⟩
[GOAL]
case mp.left.intro.mk.intro
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S s : Subsemigroup M
t : Subsemigroup N
u : Subsemigroup (M × N)
h : u ≤ prod s t
y1 : M
y2 : N
hy1 : (y1, y2) ∈ ↑u
⊢ ↑(fst M N) (y1, y2) ∈ s
[PROOFSTEP]
exact (h hy1).1
[GOAL]
case mp.right
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S s : Subsemigroup M
t : Subsemigroup N
u : Subsemigroup (M × N)
h : u ≤ prod s t
⊢ map (snd M N) u ≤ t
[PROOFSTEP]
rintro x ⟨⟨y1, y2⟩, ⟨hy1, rfl⟩⟩
[GOAL]
case mp.right.intro.mk.intro
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S s : Subsemigroup M
t : Subsemigroup N
u : Subsemigroup (M × N)
h : u ≤ prod s t
y1 : M
y2 : N
hy1 : (y1, y2) ∈ ↑u
⊢ ↑(snd M N) (y1, y2) ∈ t
[PROOFSTEP]
exact (h hy1).2
[GOAL]
case mpr
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S s : Subsemigroup M
t : Subsemigroup N
u : Subsemigroup (M × N)
⊢ map (fst M N) u ≤ s ∧ map (snd M N) u ≤ t → u ≤ prod s t
[PROOFSTEP]
rintro ⟨hH, hK⟩ ⟨x1, x2⟩ h
[GOAL]
case mpr.intro.mk
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S s : Subsemigroup M
t : Subsemigroup N
u : Subsemigroup (M × N)
hH : map (fst M N) u ≤ s
hK : map (snd M N) u ≤ t
x1 : M
x2 : N
h : (x1, x2) ∈ u
⊢ (x1, x2) ∈ prod s t
[PROOFSTEP]
exact ⟨hH ⟨_, h, rfl⟩, hK ⟨_, h, rfl⟩⟩
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S : Subsemigroup M
g : N →ₙ* P
f : M →ₙ* N
⊢ map g (srange f) = srange (comp g f)
[PROOFSTEP]
simpa only [srange_eq_map] using (⊤ : Subsemigroup M).map_map g f
[GOAL]
M : Type u_1
N✝ : Type u_2
P : Type u_3
σ : Type u_4
inst✝³ : Mul M
inst✝² : Mul N✝
inst✝¹ : Mul P
S : Subsemigroup M
N : Type u_5
inst✝ : Mul N
f : M →ₙ* N
⊢ ↑(srange f) = ↑⊤ ↔ Set.range ↑f = Set.univ
[PROOFSTEP]
rw [coe_srange, coe_top]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S : Subsemigroup M
f : M →ₙ* N
M' : Subsemigroup M
⊢ Function.Surjective ↑(subsemigroupMap f M')
[PROOFSTEP]
rintro ⟨_, x, hx, rfl⟩
[GOAL]
case mk.intro.intro
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S : Subsemigroup M
f : M →ₙ* N
M' : Subsemigroup M
x : M
hx : x ∈ ↑M'
⊢ ∃ a, ↑(subsemigroupMap f M') a = { val := ↑f x, property := (_ : ∃ a, a ∈ ↑M' ∧ ↑f a = ↑f x) }
[PROOFSTEP]
exact ⟨⟨x, hx⟩, rfl⟩
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul P
S : Subsemigroup M
inst✝¹ : Nonempty M
inst✝ : Nonempty N
s : Subsemigroup M
t : Subsemigroup N
⊢ prod s t = ⊤ ↔ s = ⊤ ∧ t = ⊤
[PROOFSTEP]
simp only [eq_top_iff, le_prod_iff, ← (gc_map_comap _).le_iff_le, ← srange_eq_map, srange_fst, srange_snd]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝¹ : Mul M
inst✝ : Mul N
S T : Subsemigroup M
f : M →ₙ* N
g : N → M
h : Function.LeftInverse g ↑f
src✝ : M →ₙ* { x // x ∈ MulHom.srange f } := MulHom.srangeRestrict f
x : { x // x ∈ MulHom.srange f }
x' : M
hx' : ↑f x' = ↑x
⊢ ↑f (g ↑x) = ↑x
[PROOFSTEP]
rw [← hx', h x']


[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : Mul M
s : Set M
inst✝ : Add A
t : Set A
p q : Subsemigroup M
h : p.carrier = q.carrier
⊢ p = q
[PROOFSTEP]
cases p
[GOAL]
case mk
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : Mul M
s : Set M
inst✝ : Add A
t : Set A
q : Subsemigroup M
carrier✝ : Set M
mul_mem'✝ : ∀ {a b : M}, a ∈ carrier✝ → b ∈ carrier✝ → a * b ∈ carrier✝
h : { carrier := carrier✝, mul_mem' := mul_mem'✝ }.carrier = q.carrier
⊢ { carrier := carrier✝, mul_mem' := mul_mem'✝ } = q
[PROOFSTEP]
cases q
[GOAL]
case mk.mk
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : Mul M
s : Set M
inst✝ : Add A
t : Set A
carrier✝¹ : Set M
mul_mem'✝¹ : ∀ {a b : M}, a ∈ carrier✝¹ → b ∈ carrier✝¹ → a * b ∈ carrier✝¹
carrier✝ : Set M
mul_mem'✝ : ∀ {a b : M}, a ∈ carrier✝ → b ∈ carrier✝ → a * b ∈ carrier✝
h : { carrier := carrier✝¹, mul_mem' := mul_mem'✝¹ }.carrier = { carrier := carrier✝, mul_mem' := mul_mem'✝ }.carrier
⊢ { carrier := carrier✝¹, mul_mem' := mul_mem'✝¹ } = { carrier := carrier✝, mul_mem' := mul_mem'✝ }
[PROOFSTEP]
congr
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : Mul M
s✝ : Set M
inst✝ : Add A
t : Set A
S : Subsemigroup M
s : Set (Subsemigroup M)
a✝ b✝ : M
hx : a✝ ∈ ⋂ (t : Subsemigroup M) (_ : t ∈ s), ↑t
hy : b✝ ∈ ⋂ (t : Subsemigroup M) (_ : t ∈ s), ↑t
i : Subsemigroup M
h : i ∈ s
⊢ a✝ ∈ i
[PROOFSTEP]
apply Set.mem_iInter₂.1 hx i h
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : Mul M
s✝ : Set M
inst✝ : Add A
t : Set A
S : Subsemigroup M
s : Set (Subsemigroup M)
a✝ b✝ : M
hx : a✝ ∈ ⋂ (t : Subsemigroup M) (_ : t ∈ s), ↑t
hy : b✝ ∈ ⋂ (t : Subsemigroup M) (_ : t ∈ s), ↑t
i : Subsemigroup M
h : i ∈ s
⊢ b✝ ∈ i
[PROOFSTEP]
apply Set.mem_iInter₂.1 hy i h
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : Mul M
s : Set M
inst✝ : Add A
t : Set A
S✝ : Subsemigroup M
ι : Sort u_4
S : ι → Subsemigroup M
x : M
⊢ x ∈ ⨅ (i : ι), S i ↔ ∀ (i : ι), x ∈ S i
[PROOFSTEP]
simp only [iInf, mem_sInf, Set.forall_range_iff]
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : Mul M
s : Set M
inst✝ : Add A
t : Set A
S✝ : Subsemigroup M
ι : Sort u_4
S : ι → Subsemigroup M
⊢ ↑(⨅ (i : ι), S i) = ⋂ (i : ι), ↑(S i)
[PROOFSTEP]
simp only [iInf, coe_sInf, Set.biInter_range]
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝² : Mul M
s : Set M
inst✝¹ : Add A
t : Set A
S : Subsemigroup M
inst✝ : Subsingleton (Subsemigroup M)
⊢ Subsingleton M
[PROOFSTEP]
constructor
[GOAL]
case allEq
M : Type u_1
N : Type u_2
A : Type u_3
inst✝² : Mul M
s : Set M
inst✝¹ : Add A
t : Set A
S : Subsemigroup M
inst✝ : Subsingleton (Subsemigroup M)
⊢ ∀ (a b : M), a = b
[PROOFSTEP]
intro x y
[GOAL]
case allEq
M : Type u_1
N : Type u_2
A : Type u_3
inst✝² : Mul M
s : Set M
inst✝¹ : Add A
t : Set A
S : Subsemigroup M
inst✝ : Subsingleton (Subsemigroup M)
x y : M
⊢ x = y
[PROOFSTEP]
have : ∀ a : M, a ∈ (⊥ : Subsemigroup M) := by simp [Subsingleton.elim (⊥ : Subsemigroup M) ⊤]
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝² : Mul M
s : Set M
inst✝¹ : Add A
t : Set A
S : Subsemigroup M
inst✝ : Subsingleton (Subsemigroup M)
x y : M
⊢ ∀ (a : M), a ∈ ⊥
[PROOFSTEP]
simp [Subsingleton.elim (⊥ : Subsemigroup M) ⊤]
[GOAL]
case allEq
M : Type u_1
N : Type u_2
A : Type u_3
inst✝² : Mul M
s : Set M
inst✝¹ : Add A
t : Set A
S : Subsemigroup M
inst✝ : Subsingleton (Subsemigroup M)
x y : M
this : ∀ (a : M), a ∈ ⊥
⊢ x = y
[PROOFSTEP]
exact absurd (this x) not_mem_bot
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : Mul M
s : Set M
inst✝ : Add A
t : Set A
S : Subsemigroup M
hn : Nonempty M
h : ⊥ = ⊤
⊢ False
[PROOFSTEP]
obtain ⟨x⟩ := id hn
[GOAL]
case intro
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : Mul M
s : Set M
inst✝ : Add A
t : Set A
S : Subsemigroup M
hn : Nonempty M
h : ⊥ = ⊤
x : M
⊢ False
[PROOFSTEP]
refine' absurd (_ : x ∈ ⊥) not_mem_bot
[GOAL]
case intro
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : Mul M
s : Set M
inst✝ : Add A
t : Set A
S : Subsemigroup M
hn : Nonempty M
h : ⊥ = ⊤
x : M
⊢ x ∈ ⊥
[PROOFSTEP]
simp [h]
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : Mul M
s✝ : Set M
inst✝ : Add A
t : Set A
S : Subsemigroup M
s : Set M
p : (x : M) → x ∈ closure s → Prop
Hs : ∀ (x : M) (h : x ∈ s), p x (_ : x ∈ ↑(closure s))
Hmul : ∀ (x : M) (hx : x ∈ closure s) (y : M) (hy : y ∈ closure s), p x hx → p y hy → p (x * y) (_ : x * y ∈ closure s)
x : M
hx : x ∈ closure s
⊢ p x hx
[PROOFSTEP]
refine' Exists.elim _ fun (hx : x ∈ closure s) (hc : p x hx) => hc
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : Mul M
s✝ : Set M
inst✝ : Add A
t : Set A
S : Subsemigroup M
s : Set M
p : (x : M) → x ∈ closure s → Prop
Hs : ∀ (x : M) (h : x ∈ s), p x (_ : x ∈ ↑(closure s))
Hmul : ∀ (x : M) (hx : x ∈ closure s) (y : M) (hy : y ∈ closure s), p x hx → p y hy → p (x * y) (_ : x * y ∈ closure s)
x : M
hx : x ∈ closure s
⊢ ∃ x_1, p x x_1
[PROOFSTEP]
exact closure_induction hx (fun x hx => ⟨_, Hs x hx⟩) fun x y ⟨hx', hx⟩ ⟨hy', hy⟩ => ⟨_, Hmul _ _ _ _ hx hy⟩
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : Mul M
s✝ : Set M
inst✝ : Add A
t : Set A
S : Subsemigroup M
p : M → Prop
x : M
s : Set M
hs : closure s = ⊤
Hs : ∀ (x : M), x ∈ s → p x
Hmul : ∀ (x y : M), p x → p y → p (x * y)
⊢ p x
[PROOFSTEP]
have : ∀ x ∈ closure s, p x := fun x hx => closure_induction hx Hs Hmul
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : Mul M
s✝ : Set M
inst✝ : Add A
t : Set A
S : Subsemigroup M
p : M → Prop
x : M
s : Set M
hs : closure s = ⊤
Hs : ∀ (x : M), x ∈ s → p x
Hmul : ∀ (x y : M), p x → p y → p (x * y)
this : ∀ (x : M), x ∈ closure s → p x
⊢ p x
[PROOFSTEP]
simpa [hs] using this x
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : Mul M
s : Set M
inst✝ : Add A
t : Set A
S : Subsemigroup M
m : M
p : Subsemigroup M
⊢ closure {m} ≤ p ↔ m ∈ p
[PROOFSTEP]
rw [closure_le, singleton_subset_iff, SetLike.mem_coe]
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : Mul M
s : Set M
inst✝ : Add A
t : Set A
S : Subsemigroup M
ι : Sort u_4
p : ι → Subsemigroup M
m : M
⊢ m ∈ ⨆ (i : ι), p i ↔ ∀ (N : Subsemigroup M), (∀ (i : ι), p i ≤ N) → m ∈ N
[PROOFSTEP]
rw [← closure_singleton_le_iff_mem, le_iSup_iff]
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : Mul M
s : Set M
inst✝ : Add A
t : Set A
S : Subsemigroup M
ι : Sort u_4
p : ι → Subsemigroup M
m : M
⊢ (∀ (b : Subsemigroup M), (∀ (i : ι), p i ≤ b) → closure {m} ≤ b) ↔
    ∀ (N : Subsemigroup M), (∀ (i : ι), p i ≤ N) → m ∈ N
[PROOFSTEP]
simp only [closure_singleton_le_iff_mem]
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : Mul M
s : Set M
inst✝ : Add A
t : Set A
S : Subsemigroup M
ι : Sort u_4
p : ι → Subsemigroup M
⊢ ⨆ (i : ι), p i = closure (⋃ (i : ι), ↑(p i))
[PROOFSTEP]
simp_rw [Subsemigroup.closure_iUnion, Subsemigroup.closure_eq]
[GOAL]
M : Type u_1
N : Type u_2
A : Type u_3
inst✝² : Mul M
s : Set M
inst✝¹ : Add A
t : Set A
inst✝ : Mul N
f g : M →ₙ* N
a✝ b✝ : M
hx : ↑f a✝ = ↑g a✝
hy : ↑f b✝ = ↑g b✝
⊢ a✝ * b✝ ∈ {x | ↑f x = ↑g x}
[PROOFSTEP]
simp [*]
[GOAL]
M✝ : Type u_1
N✝ : Type u_2
A : Type u_3
M : Type ?u.26668
N : Type ?u.26671
inst✝¹ : Semigroup M
inst✝ : Semigroup N
s : Set M
f : M → N
hs : closure s = ⊤
hmul : ∀ (x y : M), y ∈ s → f (x * y) = f x * f y
x✝ y y₁ y₂ : M
h₁ : ∀ (x : M), f (x * y₁) = f x * f y₁
h₂ : ∀ (x : M), f (x * y₂) = f x * f y₂
x : M
⊢ f (x * (y₁ * y₂)) = f x * f (y₁ * y₂)
[PROOFSTEP]
simp only [← mul_assoc, h₁, h₂]