awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
f g : Perm α
⊢ f⁻¹.Disjoint g ↔ f.Disjoint g
have refine : ∀ (h : f⁻¹.Disjoint g), f.Disjoint g
Tactic: refine ⟨fun h => ?_, Disjoint.inv_left⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
f g : Perm α
⊢ f.Disjoint g⁻¹ ↔ f.Disjoint g
have rw : g⁻¹.Disjoint f ↔ f.Disjoint g
Tactic: rw [disjoint_comm, disjoint_inv_left_iff, disjoint_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
f g : Perm α
rw : g⁻¹.Disjoint f ↔ f.Disjoint g
⊢ f.Disjoint g⁻¹ ↔ f.Disjoint g
have rw₁ : g.Disjoint f ↔ f.Disjoint g
Tactic: rw [disjoint_comm, disjoint_inv_left_iff, disjoint_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
f g : Perm α
rw : g⁻¹.Disjoint f ↔ f.Disjoint g
rw₁ : g.Disjoint f ↔ f.Disjoint g
⊢ f.Disjoint g⁻¹ ↔ f.Disjoint g
have rw₂ : f.Disjoint g ↔ f.Disjoint g
Tactic: rw [disjoint_comm, disjoint_inv_left_iff, disjoint_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
f g h : Perm α
H1 : f.Disjoint h
H2 : g.Disjoint h
x : α
⊢ (f * g : (a : α) → α) x = x ∨ (h : (a : α) → α) x = x
have inl : (f : (a : α) → α) x = x → (f * g : (a : α) → α) x = x ∨ (h : (a : α) → α) x = x
Tactic: cases H1 x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
f g h : Perm α
H1 : f.Disjoint h
H2 : g.Disjoint h
x : α
inl : (f : (a : α) → α) x = x → (f * g : (a : α) → α) x = x ∨ (h : (a : α) → α) x = x
⊢ (f * g : (a : α) → α) x = x ∨ (h : (a : α) → α) x = x
have inr : (h : (a : α) → α) x = x → (f * g : (a : α) → α) x = x ∨ (h : (a : α) → α) x = x
Tactic: cases H1 x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
f g h : Perm α
H1 : f.Disjoint h
H2 : g.Disjoint h
x : α
h_1 : (f : (a : α) → α) x = x
⊢ (f * g : (a : α) → α) x = x ∨ (h : (a : α) → α) x = x
have inl : (g : (a : α) → α) x = x → (f * g : (a : α) → α) x = x ∨ (h : (a : α) → α) x = x
Tactic: cases H2 x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
f g h : Perm α
H1 : f.Disjoint h
H2 : g.Disjoint h
x : α
h_1 : (f : (a : α) → α) x = x
inl : (g : (a : α) → α) x = x → (f * g : (a : α) → α) x = x ∨ (h : (a : α) → α) x = x
⊢ (f * g : (a : α) → α) x = x ∨ (h : (a : α) → α) x = x
have inl₁ : (h : (a : α) → α) x = x → (f * g : (a : α) → α) x = x ∨ (h : (a : α) → α) x = x
Tactic: cases H2 x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
f g h : Perm α
H1 : f.Disjoint h
H2 : g.Disjoint h
x : α
h_1 : (h : (a : α) → α) x = x
⊢ (f * g : (a : α) → α) x = x ∨ (h : (a : α) → α) x = x
have inr : (g : (a : α) → α) x = x → (f * g : (a : α) → α) x = x ∨ (h : (a : α) → α) x = x
Tactic: cases H2 x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
f g h : Perm α
H1 : f.Disjoint h
H2 : g.Disjoint h
x : α
h_1 : (h : (a : α) → α) x = x
inr : (g : (a : α) → α) x = x → (f * g : (a : α) → α) x = x ∨ (h : (a : α) → α) x = x
⊢ (f * g : (a : α) → α) x = x ∨ (h : (a : α) → α) x = x
have inr₁ : (h : (a : α) → α) x = x → (f * g : (a : α) → α) x = x ∨ (h : (a : α) → α) x = x
Tactic: cases H2 x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
f g h : Perm α
H1 : f.Disjoint g
H2 : f.Disjoint h
⊢ f.Disjoint (g * h)
have rw : (g * h).Disjoint f
Tactic: rw [disjoint_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
f : Perm α
l : List (Perm α)
h : ∀ g ∈ l, f.Disjoint g
⊢ f.Disjoint l.prod
have nil : ∀ (h : ∀ (g : Perm α), Membership.mem (γ := List (Perm α)) [] g → f.Disjoint g), f.Disjoint (List.prod [])
Tactic: induction l with
  | nil => exact disjoint_one_right _
  | cons g l ih =>
    rw [List.prod_cons]
    exact (h _ List.mem_cons_self).mul_right (ih fun g hg => h g (List.mem_cons_of_mem _ hg))
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
f : Perm α
l : List (Perm α)
h : ∀ g ∈ l, f.Disjoint g
nil : ∀ (h : ∀ (g : Perm α), Membership.mem (γ := List (Perm α)) [] g → f.Disjoint g), f.Disjoint (List.prod [])
⊢ f.Disjoint l.prod
have cons : ∀ (g : Perm α) (l : List (Perm α)) (ih : ∀ (h : ∀ g ∈ l, f.Disjoint g), f.Disjoint l.prod)
  (h : ∀ g_1 ∈ g :: l, f.Disjoint g_1), f.Disjoint (g :: l).prod
Tactic: induction l with
  | nil => exact disjoint_one_right _
  | cons g l ih =>
    rw [List.prod_cons]
    exact (h _ List.mem_cons_self).mul_right (ih fun g hg => h g (List.mem_cons_of_mem _ hg))
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
f : Perm α
x : α
hfx : (f : (a : α) → α) x = x
n : ℕ
⊢ (f ^ (n + 1) : (a : α) → α) x = x
have rw : (f ^ n * f : (a : α) → α) x = x
Tactic: rw [pow_succ, mul_apply, hfx, pow_apply_eq_self_of_apply_eq_self hfx n]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
f : Perm α
x : α
hfx : (f : (a : α) → α) x = x
n : ℕ
rw : (f ^ n * f : (a : α) → α) x = x
⊢ (f ^ (n + 1) : (a : α) → α) x = x
have rw₁ : (f ^ n : (a : α) → α) ((f : (a : α) → α) x : α) = x
Tactic: rw [pow_succ, mul_apply, hfx, pow_apply_eq_self_of_apply_eq_self hfx n]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
f : Perm α
x : α
hfx : (f : (a : α) → α) x = x
n : ℕ
rw : (f ^ n * f : (a : α) → α) x = x
rw₁ : (f ^ n : (a : α) → α) ((f : (a : α) → α) x : α) = x
⊢ (f ^ (n + 1) : (a : α) → α) x = x
have rw₂ : (f ^ n : (a : α) → α) x = x
Tactic: rw [pow_succ, mul_apply, hfx, pow_apply_eq_self_of_apply_eq_self hfx n]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
f : Perm α
x : α
hfx : (f : (a : α) → α) x = x
n : ℕ
rw : (f ^ n * f : (a : α) → α) x = x
rw₁ : (f ^ n : (a : α) → α) ((f : (a : α) → α) x : α) = x
rw₂ : (f ^ n : (a : α) → α) x = x
⊢ (f ^ (n + 1) : (a : α) → α) x = x
have rw₃ : x = x
Tactic: rw [pow_succ, mul_apply, hfx, pow_apply_eq_self_of_apply_eq_self hfx n]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
f : Perm α
x : α
hfx : (f : (a : α) → α) x = x
n : ℕ
⊢ (f ^ Int.negSucc n : (a : α) → α) x = x
have rw : ((f ^ (n + 1))⁻¹ : (a : α) → α) x = x
Tactic: rw [zpow_negSucc, inv_eq_iff_eq, pow_apply_eq_self_of_apply_eq_self hfx]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
f : Perm α
x : α
hfx : (f : (a : α) → α) x = x
n : ℕ
rw : ((f ^ (n + 1))⁻¹ : (a : α) → α) x = x
⊢ (f ^ Int.negSucc n : (a : α) → α) x = x
have rw₁ : x = (f ^ (n + 1) : (a : α) → α) x
Tactic: rw [zpow_negSucc, inv_eq_iff_eq, pow_apply_eq_self_of_apply_eq_self hfx]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
f : Perm α
x : α
hfx : (f : (a : α) → α) x = x
n : ℕ
rw : ((f ^ (n + 1))⁻¹ : (a : α) → α) x = x
rw₁ : x = (f ^ (n + 1) : (a : α) → α) x
⊢ (f ^ Int.negSucc n : (a : α) → α) x = x
have rw₂ : x = x
Tactic: rw [zpow_negSucc, inv_eq_iff_eq, pow_apply_eq_self_of_apply_eq_self hfx]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
f : Perm α
x : α
hffx : (f : (a : α) → α) ((f : (a : α) → α) x : α) = x
n : ℕ
h : (f ^ n : (a : α) → α) x = x
⊢ Eq (α := α) ((f ^ (n + 1) : (a : α) → α) x : α) ((f : (a : α) → α) x : α)
have rw : Eq (α := α) ((f * f ^ n : (a : α) → α) x : α) ((f : (a : α) → α) x : α)
Tactic: rw [pow_succ', mul_apply, h]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
f : Perm α
x : α
hffx : (f : (a : α) → α) ((f : (a : α) → α) x : α) = x
n : ℕ
h : (f ^ n : (a : α) → α) x = x
rw : Eq (α := α) ((f * f ^ n : (a : α) → α) x : α) ((f : (a : α) → α) x : α)
⊢ Eq (α := α) ((f ^ (n + 1) : (a : α) → α) x : α) ((f : (a : α) → α) x : α)
have rw₁ : Eq (α := α) ((f : (a : α) → α) ((f ^ n : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α)
Tactic: rw [pow_succ', mul_apply, h]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
f : Perm α
x : α
hffx : (f : (a : α) → α) ((f : (a : α) → α) x : α) = x
n : ℕ
h : (f ^ n : (a : α) → α) x = x
rw : Eq (α := α) ((f * f ^ n : (a : α) → α) x : α) ((f : (a : α) → α) x : α)
rw₁ : Eq (α := α) ((f : (a : α) → α) ((f ^ n : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α)
⊢ Eq (α := α) ((f ^ (n + 1) : (a : α) → α) x : α) ((f : (a : α) → α) x : α)
have rw₂ : Eq (α := α) ((f : (a : α) → α) x : α) ((f : (a : α) → α) x : α)
Tactic: rw [pow_succ', mul_apply, h]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
f : Perm α
x : α
hffx : (f : (a : α) → α) ((f : (a : α) → α) x : α) = x
n : ℕ
h : Eq (α := α) ((f ^ n : (a : α) → α) x : α) ((f : (a : α) → α) x : α)
⊢ (f ^ (n + 1) : (a : α) → α) x = x
have rw : (f * f ^ n : (a : α) → α) x = x
Tactic: rw [pow_succ', mul_apply, h, hffx]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
f : Perm α
x : α
hffx : (f : (a : α) → α) ((f : (a : α) → α) x : α) = x
n : ℕ
h : Eq (α := α) ((f ^ n : (a : α) → α) x : α) ((f : (a : α) → α) x : α)
rw : (f * f ^ n : (a : α) → α) x = x
⊢ (f ^ (n + 1) : (a : α) → α) x = x
have rw₁ : (f : (a : α) → α) ((f ^ n : (a : α) → α) x : α) = x
Tactic: rw [pow_succ', mul_apply, h, hffx]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
f : Perm α
x : α
hffx : (f : (a : α) → α) ((f : (a : α) → α) x : α) = x
n : ℕ
h : Eq (α := α) ((f ^ n : (a : α) → α) x : α) ((f : (a : α) → α) x : α)
rw : (f * f ^ n : (a : α) → α) x = x
rw₁ : (f : (a : α) → α) ((f ^ n : (a : α) → α) x : α) = x
rw₂ : (f : (a : α) → α) ((f : (a : α) → α) x : α) = x
⊢ (f ^ (n + 1) : (a : α) → α) x = x
have rw₃ : x = x
Tactic: rw [pow_succ', mul_apply, h, hffx]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
f : Perm α
x : α
hffx : (f : (a : α) → α) ((f : (a : α) → α) x : α) = x
n : ℕ
⊢ (f ^ Int.negSucc n : (a : α) → α) x = x ∨
    Eq (α := α) ((f ^ Int.negSucc n : (a : α) → α) x : α) ((f : (a : α) → α) x : α)
have rw : (f ^ (n + 1 + 1) : (a : α) → α) x = x ∨ Eq (α := α) ((f ^ (n + 1 + 1) : (a : α) → α) x : α) ((f : (a : α) → α) x : α)
Tactic: 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]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
σ τ : Perm α
hστ : σ.Disjoint τ
a : α
h : (σ : (a : α) → α) a = a ∧ (τ : (a : α) → α) a = a
⊢ (σ * τ : (a : α) → α) a = a
have rw : (σ : (a : α) → α) ((τ : (a : α) → α) a : α) = a
Tactic: rw [mul_apply, h.2, h.1]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
σ τ : Perm α
hστ : σ.Disjoint τ
a : α
h : (σ : (a : α) → α) a = a ∧ (τ : (a : α) → α) a = a
rw : (σ : (a : α) → α) ((τ : (a : α) → α) a : α) = a
⊢ (σ * τ : (a : α) → α) a = a
have rw₁ : (σ : (a : α) → α) a = a
Tactic: rw [mul_apply, h.2, h.1]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
σ τ : Perm α
hστ : σ.Disjoint τ
a : α
h : (σ : (a : α) → α) a = a ∧ (τ : (a : α) → α) a = a
rw : (σ : (a : α) → α) ((τ : (a : α) → α) a : α) = a
rw₁ : (σ : (a : α) → α) a = a
⊢ (σ * τ : (a : α) → α) a = a
have rw₂ : a = a
Tactic: rw [mul_apply, h.2, h.1]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
σ τ : Perm α
hστ : σ.Disjoint τ
a : α
⊢ (σ * τ : (a : α) → α) a = a ↔ (σ : (a : α) → α) a = a ∧ (τ : (a : α) → α) a = a
have refine : ∀ (h : (σ * τ : (a : α) → α) a = a), (σ : (a : α) → α) a = a ∧ (τ : (a : α) → α) a = a
Tactic: refine ⟨fun h => ?_, fun h => by rw [mul_apply, h.2, h.1]⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
σ τ : Perm α
hστ : σ.Disjoint τ
a : α
h : (σ * τ : (a : α) → α) a = a
⊢ (σ : (a : α) → α) a = a ∧ (τ : (a : α) → α) a = a
have inl : ∀ (hσ : (σ : (a : α) → α) a = a), (σ : (a : α) → α) a = a ∧ (τ : (a : α) → α) a = a
Tactic: rcases hστ a with hσ | hτ
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
σ τ : Perm α
hστ : σ.Disjoint τ
a : α
h : (σ * τ : (a : α) → α) a = a
inl : ∀ (hσ : (σ : (a : α) → α) a = a), (σ : (a : α) → α) a = a ∧ (τ : (a : α) → α) a = a
⊢ (σ : (a : α) → α) a = a ∧ (τ : (a : α) → α) a = a
have inr : ∀ (hτ : (τ : (a : α) → α) a = a), (σ : (a : α) → α) a = a ∧ (τ : (a : α) → α) a = a
Tactic: rcases hστ a with hσ | hτ
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
σ τ : Perm α
hστ : σ.Disjoint τ
⊢ σ * τ = 1 ↔ σ = 1 ∧ τ = 1
have simp_rw : (∀ (x : α), Eq (α := α) ((σ * τ : (a : α) → α) x : α) ((1 : (a : α) → α) x : α)) ↔
  (∀ (x : α), Eq (α := α) ((σ : (a : α) → α) x : α) ((1 : (a : α) → α) x : α)) ∧
    ∀ (x : α), Eq (α := α) ((τ : (a : α) → α) x : α) ((1 : (a : α) → α) x : α)
Tactic: simp_rw [Perm.ext_iff, one_apply, hστ.mul_apply_eq_iff, forall_and]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
σ τ : Perm α
hστ : σ.Disjoint τ
simp_rw :
  (∀ (x : α), Eq (α := α) ((σ * τ : (a : α) → α) x : α) ((1 : (a : α) → α) x : α)) ↔
    (∀ (x : α), Eq (α := α) ((σ : (a : α) → α) x : α) ((1 : (a : α) → α) x : α)) ∧
      ∀ (x : α), Eq (α := α) ((τ : (a : α) → α) x : α) ((1 : (a : α) → α) x : α)
⊢ σ * τ = 1 ↔ σ = 1 ∧ τ = 1
have simp_rw₁ : (∀ (x : α), (σ * τ : (a : α) → α) x = x) ↔ (∀ (x : α), (σ : (a : α) → α) x = x) ∧ ∀ (x : α), (τ : (a : α) → α) x = x
Tactic: simp_rw [Perm.ext_iff, one_apply, hστ.mul_apply_eq_iff, forall_and]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
σ τ : Perm α
hστ : σ.Disjoint τ
simp_rw :
  (∀ (x : α), Eq (α := α) ((σ * τ : (a : α) → α) x : α) ((1 : (a : α) → α) x : α)) ↔
    (∀ (x : α), Eq (α := α) ((σ : (a : α) → α) x : α) ((1 : (a : α) → α) x : α)) ∧
      ∀ (x : α), Eq (α := α) ((τ : (a : α) → α) x : α) ((1 : (a : α) → α) x : α)
simp_rw₁ :
  (∀ (x : α), (σ * τ : (a : α) → α) x = x) ↔ (∀ (x : α), (σ : (a : α) → α) x = x) ∧ ∀ (x : α), (τ : (a : α) → α) x = x
⊢ σ * τ = 1 ↔ σ = 1 ∧ τ = 1
have simp_rw₂ : (∀ (x : α), (σ : (a : α) → α) x = x ∧ (τ : (a : α) → α) x = x) ↔
  (∀ (x : α), (σ : (a : α) → α) x = x) ∧ ∀ (x : α), (τ : (a : α) → α) x = x
Tactic: simp_rw [Perm.ext_iff, one_apply, hστ.mul_apply_eq_iff, forall_and]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
p : α → Prop
inst_1 : DecidablePred p
f : Perm (Subtype p)
h : f.IsSwap
x : α
hx : p x
y : α
hy : p y
hxy :
  Subtype.mk (p := p) x hx ≠ Subtype.mk (p := p) y hy ∧ f = swap (Subtype.mk (p := p) x hx) (Subtype.mk (p := p) y hy)
⊢ x ≠ y
have hxy₁ : ¬x = y ∧ f = swap (Subtype.mk (p := p) x hx) (Subtype.mk (p := p) y hy)
Tactic: simp only [Ne, Subtype.ext_iff] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
p : α → Prop
inst_1 : DecidablePred p
f : Perm (Subtype p)
h : f.IsSwap
x : α
hx : p x
y : α
hy : p y
hxy :
  Subtype.mk (p := p) x hx ≠ Subtype.mk (p := p) y hy ∧ f = swap (Subtype.mk (p := p) x hx) (Subtype.mk (p := p) y hy)
⊢ (ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) f = swap x y
have rw : (ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) (swap (Subtype.mk (p := p) x hx) (Subtype.mk (p := p) y hy)) =
  swap x y
Tactic: rw [hxy.2, ofSubtype_swap_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
p : α → Prop
inst_1 : DecidablePred p
f : Perm (Subtype p)
h : f.IsSwap
x : α
hx : p x
y : α
hy : p y
hxy :
  Subtype.mk (p := p) x hx ≠ Subtype.mk (p := p) y hy ∧ f = swap (Subtype.mk (p := p) x hx) (Subtype.mk (p := p) y hy)
rw :
  (ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) (swap (Subtype.mk (p := p) x hx) (Subtype.mk (p := p) y hy)) =
    swap x y
⊢ (ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) f = swap x y
have rw₁ : swap (↑(Subtype.mk (p := p) x hx) : α) (↑(Subtype.mk (p := p) y hy) : α) = swap x y
Tactic: rw [hxy.2, ofSubtype_swap_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
f : Perm α
x y : α
hy : (swap x ((f : (a : α) → α) x) * f : (a : α) → α) y ≠ y
⊢ (f : (a : α) → α) y ≠ y ∧ y ≠ x
have hy₁ : (if (f : (a : α) → α) y = x then (f : (a : α) → α) x else if y = x then x else (f : (a : α) → α) y) ≠ y
Tactic: simp only [swap_apply_def, mul_apply, f.injective.eq_iff] at *
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
p : Perm α
⊢ Eq.{u_1 + 1} (α := Set α) {x : α | (Equiv.symm p : (a : α) → α) x ≠ x} {x : α | (p : (a : α) → α) x ≠ x}
have h : ∀ (x : α),
  Membership.mem (γ := Set α) {x : α | (Equiv.symm p : (a : α) → α) x ≠ x} x ↔
    Membership.mem (γ := Set α) {x : α | (p : (a : α) → α) x ≠ x} x
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
p q : Perm α
⊢ Subset.{u_1} (α := Set α) {x : α | (p * q : (a : α) → α) x ≠ x}
    ({x : α | (p : (a : α) → α) x ≠ x} ∪ {x : α | (q : (a : α) → α) x ≠ x})
have simp : Subset.{u_1} (α := Set α) {x : α | comp (β := α) (⇑p : (a : α) → α) (⇑q : (a : α) → α) x ≠ x}
  ({x : α | (p : (a : α) → α) x ≠ x} ∪ {x : α | (q : (a : α) → α) x ≠ x})
Tactic: simp only [coe_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
f : Perm α
n : ℕ
x : α
⊢ Eq (α := α) ((f : (a : α) → α) ((f ^ n : (a : α) → α) x : α) : α) ((f ^ n : (a : α) → α) x : α) ↔
    (f : (a : α) → α) x = x
have rw : Eq (α := α) ((f * f ^ n : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α) ↔ (f : (a : α) → α) x = x
Tactic: rw [← mul_apply, Commute.self_pow f, mul_apply, apply_eq_iff_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
f : Perm α
n : ℕ
x : α
rw : Eq (α := α) ((f * f ^ n : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α) ↔ (f : (a : α) → α) x = x
⊢ Eq (α := α) ((f : (a : α) → α) ((f ^ n : (a : α) → α) x : α) : α) ((f ^ n : (a : α) → α) x : α) ↔
    (f : (a : α) → α) x = x
have rw₁ : Eq (α := α) ((f ^ n * f : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α) ↔ (f : (a : α) → α) x = x
Tactic: rw [← mul_apply, Commute.self_pow f, mul_apply, apply_eq_iff_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
f : Perm α
n : ℕ
x : α
rw : Eq (α := α) ((f * f ^ n : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α) ↔ (f : (a : α) → α) x = x
rw₁ : Eq (α := α) ((f ^ n * f : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α) ↔ (f : (a : α) → α) x = x
⊢ Eq (α := α) ((f : (a : α) → α) ((f ^ n : (a : α) → α) x : α) : α) ((f ^ n : (a : α) → α) x : α) ↔
    (f : (a : α) → α) x = x
have rw₂ : Eq (α := α) ((f ^ n : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f ^ n : (a : α) → α) x : α) ↔
  (f : (a : α) → α) x = x
Tactic: rw [← mul_apply, Commute.self_pow f, mul_apply, apply_eq_iff_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
f : Perm α
n : ℕ
x : α
rw : Eq (α := α) ((f * f ^ n : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α) ↔ (f : (a : α) → α) x = x
rw₁ : Eq (α := α) ((f ^ n * f : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α) ↔ (f : (a : α) → α) x = x
rw₂ :
  Eq (α := α) ((f ^ n : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f ^ n : (a : α) → α) x : α) ↔
    (f : (a : α) → α) x = x
⊢ Eq (α := α) ((f : (a : α) → α) ((f ^ n : (a : α) → α) x : α) : α) ((f ^ n : (a : α) → α) x : α) ↔
    (f : (a : α) → α) x = x
have rw₃ : (f : (a : α) → α) x = x ↔ (f : (a : α) → α) x = x
Tactic: rw [← mul_apply, Commute.self_pow f, mul_apply, apply_eq_iff_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
f : Perm α
n : ℤ
x : α
⊢ Eq (α := α) ((f : (a : α) → α) ((f ^ n : (a : α) → α) x : α) : α) ((f ^ n : (a : α) → α) x : α) ↔
    (f : (a : α) → α) x = x
have rw : Eq (α := α) ((f * f ^ n : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α) ↔ (f : (a : α) → α) x = x
Tactic: rw [← mul_apply, Commute.self_zpow f, mul_apply, apply_eq_iff_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
f : Perm α
n : ℤ
x : α
rw : Eq (α := α) ((f * f ^ n : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α) ↔ (f : (a : α) → α) x = x
⊢ Eq (α := α) ((f : (a : α) → α) ((f ^ n : (a : α) → α) x : α) : α) ((f ^ n : (a : α) → α) x : α) ↔
    (f : (a : α) → α) x = x
have rw₁ : Eq (α := α) ((f ^ n * f : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α) ↔ (f : (a : α) → α) x = x
Tactic: rw [← mul_apply, Commute.self_zpow f, mul_apply, apply_eq_iff_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
f : Perm α
n : ℤ
x : α
rw : Eq (α := α) ((f * f ^ n : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α) ↔ (f : (a : α) → α) x = x
rw₁ : Eq (α := α) ((f ^ n * f : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α) ↔ (f : (a : α) → α) x = x
⊢ Eq (α := α) ((f : (a : α) → α) ((f ^ n : (a : α) → α) x : α) : α) ((f ^ n : (a : α) → α) x : α) ↔
    (f : (a : α) → α) x = x
have rw₂ : Eq (α := α) ((f ^ n : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f ^ n : (a : α) → α) x : α) ↔
  (f : (a : α) → α) x = x
Tactic: rw [← mul_apply, Commute.self_zpow f, mul_apply, apply_eq_iff_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
f : Perm α
n : ℤ
x : α
rw : Eq (α := α) ((f * f ^ n : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α) ↔ (f : (a : α) → α) x = x
rw₁ : Eq (α := α) ((f ^ n * f : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α) ↔ (f : (a : α) → α) x = x
rw₂ :
  Eq (α := α) ((f ^ n : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f ^ n : (a : α) → α) x : α) ↔
    (f : (a : α) → α) x = x
⊢ Eq (α := α) ((f : (a : α) → α) ((f ^ n : (a : α) → α) x : α) : α) ((f ^ n : (a : α) → α) x : α) ↔
    (f : (a : α) → α) x = x
have rw₃ : (f : (a : α) → α) x = x ↔ (f : (a : α) → α) x = x
Tactic: rw [← mul_apply, Commute.self_zpow f, mul_apply, apply_eq_iff_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x : α
⊢ x ∈ f.support ↔ (f : (a : α) → α) x ≠ x
have rw : Membership.mem (γ := Finset α) {x : α | (f : (a : α) → α) x ≠ x} x ↔ (f : (a : α) → α) x ≠ x
Tactic: rw [support, mem_filter, and_iff_right (mem_univ x)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x : α
rw : Membership.mem (γ := Finset α) {x : α | (f : (a : α) → α) x ≠ x} x ↔ (f : (a : α) → α) x ≠ x
⊢ x ∈ f.support ↔ (f : (a : α) → α) x ≠ x
have rw₁ : Membership.mem (γ := Finset α) univ x ∧ (f : (a : α) → α) x ≠ x ↔ (f : (a : α) → α) x ≠ x
Tactic: rw [support, mem_filter, and_iff_right (mem_univ x)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x : α
rw : Membership.mem (γ := Finset α) {x : α | (f : (a : α) → α) x ≠ x} x ↔ (f : (a : α) → α) x ≠ x
rw₁ : Membership.mem (γ := Finset α) univ x ∧ (f : (a : α) → α) x ≠ x ↔ (f : (a : α) → α) x ≠ x
⊢ x ∈ f.support ↔ (f : (a : α) → α) x ≠ x
have rw₂ : (f : (a : α) → α) x ≠ x ↔ (f : (a : α) → α) x ≠ x
Tactic: rw [support, mem_filter, and_iff_right (mem_univ x)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
⊢ (↑f.support : Set α) = {x : α | (f : (a : α) → α) x ≠ x}
have h : ∀ (x : α), x ∈ (↑f.support : Set α) ↔ Membership.mem (γ := Set α) {x : α | (f : (a : α) → α) x ≠ x} x
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
⊢ σ.support = ∅ ↔ σ = 1
have simp_rw : (∀ (a : α), a ∈ σ.support ↔ Membership.mem (γ := Finset α) ∅ a) ↔ σ = 1
Tactic: simp_rw [Finset.ext_iff, mem_support, Finset.notMem_empty, iff_false, not_not,
    Equiv.Perm.ext_iff, one_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
simp_rw : (∀ (a : α), a ∈ σ.support ↔ Membership.mem (γ := Finset α) ∅ a) ↔ σ = 1
⊢ σ.support = ∅ ↔ σ = 1
have simp_rw₁ : (∀ (a : α), (σ : (a : α) → α) a ≠ a ↔ Membership.mem (γ := Finset α) ∅ a) ↔ σ = 1
Tactic: simp_rw [Finset.ext_iff, mem_support, Finset.notMem_empty, iff_false, not_not,
    Equiv.Perm.ext_iff, one_apply]