awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
simp_rw₁ : (∀ (a : α), (σ : (a : α) → α) a ≠ a ↔ Membership.mem (γ := Finset α) ∅ a) ↔ σ = 1
⊢ σ.support = ∅ ↔ σ = 1
have simp_rw₂ : (∀ (a : α), (σ : (a : α) → α) a ≠ a ↔ False) ↔ σ = 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
simp_rw₁ : (∀ (a : α), (σ : (a : α) → α) a ≠ a ↔ Membership.mem (γ := Finset α) ∅ a) ↔ σ = 1
simp_rw₂ : (∀ (a : α), (σ : (a : α) → α) a ≠ a ↔ False) ↔ σ = 1
⊢ σ.support = ∅ ↔ σ = 1
have simp_rw₃ : (∀ (a : α), ¬(σ : (a : α) → α) a ≠ 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
simp_rw₁ : (∀ (a : α), (σ : (a : α) → α) a ≠ a ↔ Membership.mem (γ := Finset α) ∅ a) ↔ σ = 1
simp_rw₂ : (∀ (a : α), (σ : (a : α) → α) a ≠ a ↔ False) ↔ σ = 1
simp_rw₃ : (∀ (a : α), ¬(σ : (a : α) → α) a ≠ a) ↔ σ = 1
⊢ σ.support = ∅ ↔ σ = 1
have simp_rw₄ : (∀ (a : α), (σ : (a : α) → α) a = 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
simp_rw₁ : (∀ (a : α), (σ : (a : α) → α) a ≠ a ↔ Membership.mem (γ := Finset α) ∅ a) ↔ σ = 1
simp_rw₂ : (∀ (a : α), (σ : (a : α) → α) a ≠ a ↔ False) ↔ σ = 1
simp_rw₃ : (∀ (a : α), ¬(σ : (a : α) → α) a ≠ a) ↔ σ = 1
simp_rw₄ : (∀ (a : α), (σ : (a : α) → α) a = a) ↔ σ = 1
⊢ σ.support = ∅ ↔ σ = 1
have simp_rw₅ : (∀ (a : α), (σ : (a : α) → α) a = a) ↔ ∀ (x : α), Eq (α := α) ((σ : (a : α) → α) x : α) ((1 : (a : α) → α) x : α)
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 α
⊢ Eq.{u_1 + 1} (α := Finset α) (support 1) ∅
have rw : Eq.{u_1 + 1} (α := Perm α) 1 1
Tactic: rw [support_eq_empty_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
hgc : Commute g c
x : α
⊢ Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support
have simp : Eq (α := α) ((c * g : (a : α) → α) x : α) ((g : (a : α) → α) x : α) ↔ (c : (a : α) → α) x = x
Tactic: simp only [mem_support, not_iff_not, ← mul_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
hgc : Commute g c
x : α
⊢ Eq (α := α) ((c * g : (a : α) → α) x : α) ((g : (a : α) → α) x : α) ↔ (c : (a : α) → α) x = x
have rw : Eq (α := α) ((g * c : (a : α) → α) x : α) ((g : (a : α) → α) x : α) ↔ (c : (a : α) → α) x = x
Tactic: rw [← hgc, mul_apply, Equiv.apply_eq_iff_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
hgc : Commute g c
x : α
rw : Eq (α := α) ((g * c : (a : α) → α) x : α) ((g : (a : α) → α) x : α) ↔ (c : (a : α) → α) x = x
⊢ Eq (α := α) ((c * g : (a : α) → α) x : α) ((g : (a : α) → α) x : α) ↔ (c : (a : α) → α) x = x
have rw₁ : Eq (α := α) ((g : (a : α) → α) ((c : (a : α) → α) x : α) : α) ((g : (a : α) → α) x : α) ↔ (c : (a : α) → α) x = x
Tactic: rw [← hgc, mul_apply, Equiv.apply_eq_iff_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
hgc : Commute g c
x : α
rw : Eq (α := α) ((g * c : (a : α) → α) x : α) ((g : (a : α) → α) x : α) ↔ (c : (a : α) → α) x = x
rw₁ : Eq (α := α) ((g : (a : α) → α) ((c : (a : α) → α) x : α) : α) ((g : (a : α) → α) x : α) ↔ (c : (a : α) → α) x = x
⊢ Eq (α := α) ((c * g : (a : α) → α) x : α) ((g : (a : α) → α) x : α) ↔ (c : (a : α) → α) x = x
have rw₂ : (c : (a : α) → α) x = x ↔ (c : (a : α) → α) x = x
Tactic: rw [← hgc, mul_apply, Equiv.apply_eq_iff_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
x : α
⊢ x ∈ (f * g).support → x ∈ f.support ∪ g.support
have rw : (f : (a : α) → α) x = x ∧ (g : (a : α) → α) x = x → (f : (a : α) → α) ((g : (a : α) → α) x : α) = x
Tactic: rw [mem_union, mem_support, mem_support, mem_support, mul_apply, ← not_and_or, not_imp_not]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
x : α
hf : (f : (a : α) → α) x = x
hg : (g : (a : α) → α) x = x
rw : (f : (a : α) → α) x = x
⊢ (f : (a : α) → α) ((g : (a : α) → α) x : α) = x
have rw₁ : x = x
Tactic: rw [hg, hf]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
l : List (Perm α)
x : α
hx : x ∈ l.prod.support
⊢ ∃ f ∈ l, x ∈ f.support
have contrapose! : ∀ (hx : ∀ (f : Perm α) (_ : f ∈ l), x ∉ f.support), x ∉ l.prod.support
Tactic: contrapose! hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
l : List (Perm α)
x : α
hx : ∀ (f : Perm α) (_ : f ∈ l), x ∉ f.support
⊢ x ∉ l.prod.support
have simp_rw : ∀ (hx : ∀ (f : Perm α) (_ : f ∈ l), (f : (a : α) → α) x = x), (l.prod : (a : α) → α) x = x
Tactic: simp_rw [mem_support, not_not] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
x : α
f : Perm α
l : List (Perm α)
ih : ∀ (hx : ∀ (f : Perm α) (_ : f ∈ l), (f : (a : α) → α) x = x), (l.prod : (a : α) → α) x = x
hx : ∀ (f_1 : Perm α) (_ : f_1 ∈ f :: l), (f_1 : (a : α) → α) x = x
⊢ ((f :: l).prod : (a : α) → α) x = x
have cons : f ∈ f :: l
Tactic: rw [List.prod_cons, mul_apply, ih, hx]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
x : α
f : Perm α
l : List (Perm α)
ih : ∀ (hx : ∀ (f : Perm α) (_ : f ∈ l), (f : (a : α) → α) x = x), (l.prod : (a : α) → α) x = x
hx : ∀ (f_1 : Perm α) (_ : f_1 ∈ f :: l), (f_1 : (a : α) → α) x = x
cons : f ∈ f :: l
⊢ ((f :: l).prod : (a : α) → α) x = x
have cons₁ : ∀ (f : Perm α) (_ : f ∈ l), (f : (a : α) → α) x = x
Tactic: rw [List.prod_cons, mul_apply, ih, hx]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
l : List (Perm α)
x : α
hx : ∀ (f : Perm α) (_ : f ∈ l), (f : (a : α) → α) x = x
⊢ (l.prod : (a : α) → α) x = x
have nil : ∀ (hx : ∀ (f : Perm α) (_ : Membership.mem (γ := List (Perm α)) [] f), (f : (a : α) → α) x = x),
  (List.prod [] : (a : α) → α) x = x
Tactic: induction l with
  | nil => rfl
  | cons f l ih =>
    rw [List.prod_cons, mul_apply, ih, hx]
    · simp only [List.mem_cons, true_or]
    grind
Cleared hypotheses: l, hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
l : List (Perm α)
x : α
hx : ∀ (f : Perm α) (_ : f ∈ l), (f : (a : α) → α) x = x
nil :
  ∀ (hx : ∀ (f : Perm α) (_ : Membership.mem (γ := List (Perm α)) [] f), (f : (a : α) → α) x = x),
    (List.prod [] : (a : α) → α) x = x
⊢ (l.prod : (a : α) → α) x = x
have cons : ∀ (f : Perm α) (l : List (Perm α))
  (ih : ∀ (hx : ∀ (f : Perm α) (_ : f ∈ l), (f : (a : α) → α) x = x), (l.prod : (a : α) → α) x = x)
  (hx : ∀ (f_1 : Perm α) (_ : f_1 ∈ f :: l), (f_1 : (a : α) → α) x = x), ((f :: l).prod : (a : α) → α) x = x
Tactic: induction l with
  | nil => rfl
  | cons f l ih =>
    rw [List.prod_cons, mul_apply, ih, hx]
    · simp only [List.mem_cons, true_or]
    grind
Cleared hypotheses: l, hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
⊢ σ⁻¹.support = σ.support
have simp_rw : ∀ (a : α), a ∈ σ⁻¹.support ↔ a ∈ σ.support
Tactic: simp_rw [Finset.ext_iff, mem_support, not_iff_not, inv_eq_iff_eq.trans eq_comm, imp_true_iff]
-- 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 ↔ a ∈ σ.support
⊢ σ⁻¹.support = σ.support
have simp_rw₁ : ∀ (a : α), (σ⁻¹ : (a : α) → α) a ≠ a ↔ (σ : (a : α) → α) a ≠ a
Tactic: simp_rw [Finset.ext_iff, mem_support, not_iff_not, inv_eq_iff_eq.trans eq_comm, imp_true_iff]
-- 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 ↔ a ∈ σ.support
simp_rw₁ : ∀ (a : α), (σ⁻¹ : (a : α) → α) a ≠ a ↔ (σ : (a : α) → α) a ≠ a
⊢ σ⁻¹.support = σ.support
have simp_rw₂ : ∀ (a : α), (σ⁻¹ : (a : α) → α) a = a ↔ (σ : (a : α) → α) a = a
Tactic: simp_rw [Finset.ext_iff, mem_support, not_iff_not, inv_eq_iff_eq.trans eq_comm, imp_true_iff]
-- 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 ↔ a ∈ σ.support
simp_rw₁ : ∀ (a : α), (σ⁻¹ : (a : α) → α) a ≠ a ↔ (σ : (a : α) → α) a ≠ a
simp_rw₂ : ∀ (a : α), (σ⁻¹ : (a : α) → α) a = a ↔ (σ : (a : α) → α) a = a
⊢ σ⁻¹.support = σ.support
have simp_rw₃ : ∀ (a : α), True
Tactic: simp_rw [Finset.ext_iff, mem_support, not_iff_not, inv_eq_iff_eq.trans eq_comm, imp_true_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x : α
⊢ Membership.mem (α := α) f.support ((f : (a : α) → α) x : α) ↔ x ∈ f.support
have rw : Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α) ↔ x ∈ f.support
Tactic: rw [mem_support, mem_support, Ne, Ne, 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 : α
rw : Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α) ↔ x ∈ f.support
⊢ Membership.mem (α := α) f.support ((f : (a : α) → α) x : α) ↔ x ∈ f.support
have rw₁ : Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α) ↔ (f : (a : α) → α) x ≠ x
Tactic: rw [mem_support, mem_support, Ne, Ne, 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 : α
rw : Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α) ↔ x ∈ f.support
rw₁ : Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α) ↔ (f : (a : α) → α) x ≠ x
⊢ Membership.mem (α := α) f.support ((f : (a : α) → α) x : α) ↔ x ∈ f.support
have rw₂ : ¬Eq (α := α) ((f : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α) ↔ (f : (a : α) → α) x ≠ x
Tactic: rw [mem_support, mem_support, Ne, Ne, 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 : α
rw : Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α) ↔ x ∈ f.support
rw₁ : Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α) ↔ (f : (a : α) → α) x ≠ x
rw₂ : ¬Eq (α := α) ((f : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α) ↔ (f : (a : α) → α) x ≠ x
⊢ Membership.mem (α := α) f.support ((f : (a : α) → α) x : α) ↔ x ∈ f.support
have rw₃ : ¬Eq (α := α) ((f : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α) ↔ ¬(f : (a : α) → α) x = x
Tactic: rw [mem_support, mem_support, Ne, Ne, 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 : α
rw : Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α) ↔ x ∈ f.support
rw₁ : Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α) ↔ (f : (a : α) → α) x ≠ x
rw₂ : ¬Eq (α := α) ((f : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α) ↔ (f : (a : α) → α) x ≠ x
rw₃ :
  ¬Eq (α := α) ((f : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α) ↔ ¬(f : (a : α) → α) x = x
⊢ Membership.mem (α := α) f.support ((f : (a : α) → α) x : α) ↔ x ∈ f.support
have rw₄ : ¬(f : (a : α) → α) x = x ↔ ¬(f : (a : α) → α) x = x
Tactic: rw [mem_support, mem_support, Ne, Ne, apply_eq_iff_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
c : Perm α
s : Finset α
hcs : c.support ≤ s
x : α
⊢ Membership.mem (α := α) s ((c : (a : α) → α) x : α) ↔ x ∈ s
have pos : ∀ (hx' : x ∈ c.support), Membership.mem (α := α) s ((c : (a : α) → α) x : α) ↔ x ∈ s
Tactic: by_cases hx' : x ∈ c.support
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
c : Perm α
s : Finset α
hcs : c.support ≤ s
x : α
pos : ∀ (hx' : x ∈ c.support), Membership.mem (α := α) s ((c : (a : α) → α) x : α) ↔ x ∈ s
⊢ Membership.mem (α := α) s ((c : (a : α) → α) x : α) ↔ x ∈ s
have neg : ∀ (hx' : x ∉ c.support), Membership.mem (α := α) s ((c : (a : α) → α) x : α) ↔ x ∈ s
Tactic: by_cases hx' : x ∈ c.support
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
c : Perm α
s : Finset α
hcs : c.support ≤ s
x : α
hx' : x ∉ c.support
⊢ Membership.mem (α := α) s ((c : (a : α) → α) x : α) ↔ x ∈ s
have neg : x ∈ s ↔ x ∈ s
Tactic: rw [notMem_support.mp hx']
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), Membership.mem (α := α) s ((g : (a : α) → α) x : α) ↔ x ∈ s
⊢ (ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (g.subtypePerm (p := Membership.mem s) hg) = c ↔
    c.support ≤ s ∧
      ∀ (hc' : ∀ (x : α), Membership.mem (α := α) s ((c : (a : α) → α) x : α) ↔ x ∈ s),
        c.subtypePerm (p := Membership.mem s) hc' = g.subtypePerm (p := Membership.mem s) hg
have simp : (∀ (x : α),
    Eq (α := α)
      ((((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (g.subtypePerm (p := Membership.mem s) hg) :
              Perm α) :
            (a : α) → α)
          x :
        α)
      ((c : (a : α) → α) x : α)) ↔
  c.support ≤ s ∧
    ∀ (hc' : ∀ (x : α), Membership.mem (α := α) s ((c : (a : α) → α) x : α) ↔ x ∈ s) (a : α) (b : a ∈ s),
      Eq (α := α) ((c : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
Tactic: simp only [Equiv.ext_iff, subtypePerm_apply, Subtype.mk.injEq, Subtype.forall]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), Membership.mem (α := α) s ((g : (a : α) → α) x : α) ↔ x ∈ s
⊢ (∀ (x : α),
      Eq (α := α)
        ((((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (g.subtypePerm (p := Membership.mem s) hg) :
                Perm α) :
              (a : α) → α)
            x :
          α)
        ((c : (a : α) → α) x : α)) ↔
    c.support ≤ s ∧
      ∀ (hc' : ∀ (x : α), Membership.mem (α := α) s ((c : (a : α) → α) x : α) ↔ x ∈ s) (a : α) (b : a ∈ s),
        Eq (α := α) ((c : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
have mp : (∀ (x : α),
    Eq (α := α)
      ((((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (g.subtypePerm (p := Membership.mem s) hg) :
              Perm α) :
            (a : α) → α)
          x :
        α)
      ((c : (a : α) → α) x : α)) →
  c.support ≤ s ∧
    ∀ (hc' : ∀ (x : α), Membership.mem (α := α) s ((c : (a : α) → α) x : α) ↔ x ∈ s) (a : α) (b : a ∈ s),
      Eq (α := α) ((c : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), Membership.mem (α := α) s ((g : (a : α) → α) x : α) ↔ x ∈ s
mp :
  (∀ (x : α),
      Eq (α := α)
        ((((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (g.subtypePerm (p := Membership.mem s) hg) :
                Perm α) :
              (a : α) → α)
            x :
          α)
        ((c : (a : α) → α) x : α)) →
    c.support ≤ s ∧
      ∀ (hc' : ∀ (x : α), Membership.mem (α := α) s ((c : (a : α) → α) x : α) ↔ x ∈ s) (a : α) (b : a ∈ s),
        Eq (α := α) ((c : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
⊢ (∀ (x : α),
      Eq (α := α)
        ((((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (g.subtypePerm (p := Membership.mem s) hg) :
                Perm α) :
              (a : α) → α)
            x :
          α)
        ((c : (a : α) → α) x : α)) ↔
    c.support ≤ s ∧
      ∀ (hc' : ∀ (x : α), Membership.mem (α := α) s ((c : (a : α) → α) x : α) ↔ x ∈ s) (a : α) (b : a ∈ s),
        Eq (α := α) ((c : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
have mpr : (c.support ≤ s ∧
    ∀ (hc' : ∀ (x : α), Membership.mem (α := α) s ((c : (a : α) → α) x : α) ↔ x ∈ s) (a : α) (b : a ∈ s),
      Eq (α := α) ((c : (a : α) → α) a : α) ((g : (a : α) → α) a : α)) →
  ∀ (x : α),
    Eq (α := α)
      ((((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (g.subtypePerm (p := Membership.mem s) hg) :
              Perm α) :
            (a : α) → α)
          x :
        α)
      ((c : (a : α) → α) x : α)
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), Membership.mem (α := α) s ((g : (a : α) → α) x : α) ↔ x ∈ s
h :
  ∀ (x : α),
    Eq (α := α)
      ((((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (g.subtypePerm (p := Membership.mem s) hg) :
              Perm α) :
            (a : α) → α)
          x :
        α)
      ((c : (a : α) → α) x : α)
⊢ c.support ≤ s ∧
    ∀ (hc' : ∀ (x : α), Membership.mem (α := α) s ((c : (a : α) → α) x : α) ↔ x ∈ s) (a : α) (b : a ∈ s),
      Eq (α := α) ((c : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
have mp : c.support ≤ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), Membership.mem (α := α) s ((g : (a : α) → α) x : α) ↔ x ∈ s
h :
  ∀ (x : α),
    Eq (α := α)
      ((((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (g.subtypePerm (p := Membership.mem s) hg) :
              Perm α) :
            (a : α) → α)
          x :
        α)
      ((c : (a : α) → α) x : α)
mp : c.support ≤ s
⊢ c.support ≤ s ∧
    ∀ (hc' : ∀ (x : α), Membership.mem (α := α) s ((c : (a : α) → α) x : α) ↔ x ∈ s) (a : α) (b : a ∈ s),
      Eq (α := α) ((c : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
have mp₁ : ∀ (hc' : ∀ (x : α), Membership.mem (α := α) s ((c : (a : α) → α) x : α) ↔ x ∈ s) (a : α) (b : a ∈ s),
  Eq (α := α) ((c : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), Membership.mem (α := α) s ((g : (a : α) → α) x : α) ↔ x ∈ s
h :
  ∀ (x : α),
    Eq (α := α)
      ((((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (g.subtypePerm (p := Membership.mem s) hg) :
              Perm α) :
            (a : α) → α)
          x :
        α)
      ((c : (a : α) → α) x : α)
a : α
ha : a ∈ c.support
⊢ a ∈ s
have mp : ∀ (ha' : a ∉ s), False
Tactic: by_contra ha'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), Membership.mem (α := α) s ((g : (a : α) → α) x : α) ↔ x ∈ s
h :
  ∀ (x : α),
    Eq (α := α)
      ((((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (g.subtypePerm (p := Membership.mem s) hg) :
              Perm α) :
            (a : α) → α)
          x :
        α)
      ((c : (a : α) → α) x : α)
a : α
ha : a ∈ c.support
ha' : a ∉ s
⊢ False
have ha₁ : a ≠ a
Tactic: rw [mem_support, ← h a, ofSubtype_apply_of_not_mem (p := (· ∈ s)) _ ha'] at ha
Cleared hypotheses: ha, ha'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), Membership.mem (α := α) s ((g : (a : α) → α) x : α) ↔ x ∈ s
h :
  ∀ (x : α),
    Eq (α := α)
      ((((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (g.subtypePerm (p := Membership.mem s) hg) :
              Perm α) :
            (a : α) → α)
          x :
        α)
      ((c : (a : α) → α) x : α)
hc' : ∀ (x : α), Membership.mem (α := α) s ((c : (a : α) → α) x : α) ↔ x ∈ s
a : α
ha : a ∈ s
⊢ Eq (α := α) ((c : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
have mp : Eq (α := α)
  ((((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (g.subtypePerm (p := Membership.mem s) hg) :
          Perm α) :
        (a : α) → α)
      a :
    α)
  ((g : (a : α) → α) a : α)
Tactic: rw [← h a, ofSubtype_apply_of_mem (p := (· ∈ s)) _ ha, subtypePerm_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), Membership.mem (α := α) s ((g : (a : α) → α) x : α) ↔ x ∈ s
h :
  ∀ (x : α),
    Eq (α := α)
      ((((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (g.subtypePerm (p := Membership.mem s) hg) :
              Perm α) :
            (a : α) → α)
          x :
        α)
      ((c : (a : α) → α) x : α)
hc' : ∀ (x : α), Membership.mem (α := α) s ((c : (a : α) → α) x : α) ↔ x ∈ s
a : α
ha : a ∈ s
mp :
  Eq (α := α)
    ((((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (g.subtypePerm (p := Membership.mem s) hg) :
            Perm α) :
          (a : α) → α)
        a :
      α)
    ((g : (a : α) → α) a : α)
⊢ Eq (α := α) ((c : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
have mp₁ : Eq (α := α)
  ((↑((g.subtypePerm (p := Membership.mem s) hg : (a : ↥s) → ↥s) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha)) : α) : α)
  ((g : (a : α) → α) a : α)
Tactic: rw [← h a, ofSubtype_apply_of_mem (p := (· ∈ s)) _ ha, subtypePerm_apply]