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 α
f hd : Perm α
tl : List (Perm α)
IH :
  ∀ (h : f ∈ tl) (hl : List.Pairwise Disjoint tl),
    ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((tl.prod : (a : α) → α) x : α)
h : f ∈ hd :: tl
hl : (∀ a' ∈ tl, hd.Disjoint a') ∧ List.Pairwise Disjoint tl
x : α
hx : x ∈ f.support
⊢ Eq (α := α) ((f : (a : α) → α) x : α) (((hd :: tl).prod : (a : α) → α) x : α)
have cons : ∀ (h : f = hd ∨ f ∈ tl) (hl : (∀ a' ∈ tl, hd.Disjoint a') ∧ List.Pairwise Disjoint tl) (x : α) (hx : x ∈ f.support),
  Eq (α := α) ((f : (a : α) → α) x : α) (((hd :: tl).prod : (a : α) → α) x : α)
Tactic: rw [List.mem_cons] at h
Cleared hypotheses: h, hl, x, hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f hd : Perm α
tl : List (Perm α)
IH :
  ∀ (h : f ∈ tl) (hl : List.Pairwise Disjoint tl),
    ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((tl.prod : (a : α) → α) x : α)
h : f = hd ∨ f ∈ tl
hl : (∀ a' ∈ tl, hd.Disjoint a') ∧ List.Pairwise Disjoint tl
x : α
hx : x ∈ f.support
⊢ Eq (α := α) ((f : (a : α) → α) x : α) (((hd :: tl).prod : (a : α) → α) x : α)
have cons : ∀ (hl : (∀ a' ∈ tl, f.Disjoint a') ∧ List.Pairwise Disjoint tl),
  Eq (α := α) ((f : (a : α) → α) x : α) (((f :: tl).prod : (a : α) → α) x : α)
Tactic: rcases h with (rfl | h)
Cleared hypotheses: hd, h, hl
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f hd : Perm α
tl : List (Perm α)
IH :
  ∀ (h : f ∈ tl) (hl : List.Pairwise Disjoint tl),
    ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((tl.prod : (a : α) → α) x : α)
h : f = hd ∨ f ∈ tl
hl : (∀ a' ∈ tl, hd.Disjoint a') ∧ List.Pairwise Disjoint tl
x : α
hx : x ∈ f.support
cons :
  ∀ (hl : (∀ a' ∈ tl, f.Disjoint a') ∧ List.Pairwise Disjoint tl),
    Eq (α := α) ((f : (a : α) → α) x : α) (((f :: tl).prod : (a : α) → α) x : α)
⊢ Eq (α := α) ((f : (a : α) → α) x : α) (((hd :: tl).prod : (a : α) → α) x : α)
have cons₁ : ∀ (h : f ∈ tl), Eq (α := α) ((f : (a : α) → α) x : α) (((hd :: tl).prod : (a : α) → α) x : α)
Tactic: rcases h with (rfl | h)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
tl : List (Perm α)
IH :
  ∀ (h : f ∈ tl) (hl : List.Pairwise Disjoint tl),
    ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((tl.prod : (a : α) → α) x : α)
x : α
hx : x ∈ f.support
hl : (∀ a' ∈ tl, f.Disjoint a') ∧ List.Pairwise Disjoint tl
⊢ Eq (α := α) ((f : (a : α) → α) x : α) (((f :: tl).prod : (a : α) → α) x : α)
have cons : Eq (α := α) ((f : (a : α) → α) x : α) ((f * tl.prod : (a : α) → α) x : α)
Tactic: rw [List.prod_cons, mul_apply,
        notMem_support.mp ((disjoint_prod_right tl hl.left).mem_imp hx)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
tl : List (Perm α)
IH :
  ∀ (h : f ∈ tl) (hl : List.Pairwise Disjoint tl),
    ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((tl.prod : (a : α) → α) x : α)
x : α
hx : x ∈ f.support
hl : (∀ a' ∈ tl, f.Disjoint a') ∧ List.Pairwise Disjoint tl
cons : Eq (α := α) ((f : (a : α) → α) x : α) ((f * tl.prod : (a : α) → α) x : α)
⊢ Eq (α := α) ((f : (a : α) → α) x : α) (((f :: tl).prod : (a : α) → α) x : α)
have cons₁ : Eq (α := α) ((f : (a : α) → α) x : α) ((f : (a : α) → α) ((tl.prod : (a : α) → α) x : α) : α)
Tactic: rw [List.prod_cons, mul_apply,
        notMem_support.mp ((disjoint_prod_right tl hl.left).mem_imp hx)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
tl : List (Perm α)
IH :
  ∀ (h : f ∈ tl) (hl : List.Pairwise Disjoint tl),
    ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((tl.prod : (a : α) → α) x : α)
x : α
hx : x ∈ f.support
hl : (∀ a' ∈ tl, f.Disjoint a') ∧ List.Pairwise Disjoint tl
cons : Eq (α := α) ((f : (a : α) → α) x : α) ((f * tl.prod : (a : α) → α) x : α)
cons₁ : Eq (α := α) ((f : (a : α) → α) x : α) ((f : (a : α) → α) ((tl.prod : (a : α) → α) x : α) : α)
⊢ Eq (α := α) ((f : (a : α) → α) x : α) (((f :: tl).prod : (a : α) → α) x : α)
have cons₂ : Eq (α := α) ((f : (a : α) → α) x : α) ((f : (a : α) → α) x : α)
Tactic: rw [List.prod_cons, mul_apply,
        notMem_support.mp ((disjoint_prod_right tl hl.left).mem_imp hx)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f hd : Perm α
tl : List (Perm α)
IH :
  ∀ (h : f ∈ tl) (hl : List.Pairwise Disjoint tl),
    ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((tl.prod : (a : α) → α) x : α)
hl : (∀ a' ∈ tl, hd.Disjoint a') ∧ List.Pairwise Disjoint tl
x : α
hx : x ∈ f.support
h : f ∈ tl
⊢ Eq (α := α) ((f : (a : α) → α) x : α) (((hd :: tl).prod : (a : α) → α) x : α)
have cons : ((f : (a : α) → α) x : α) ∉ hd.support
Tactic: rw [List.prod_cons, mul_apply, ← IH h hl.right _ hx, eq_comm, ← notMem_support]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f hd : Perm α
tl : List (Perm α)
IH :
  ∀ (h : f ∈ tl) (hl : List.Pairwise Disjoint tl),
    ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((tl.prod : (a : α) → α) x : α)
hl : (∀ a' ∈ tl, hd.Disjoint a') ∧ List.Pairwise Disjoint tl
x : α
hx : x ∈ f.support
h : f ∈ tl
⊢ ((f : (a : α) → α) x : α) ∉ hd.support
have cons : Membership.mem (α := α) f.support ((f : (a : α) → α) x : α)
Tactic: refine (hl.left _ h).symm.mem_imp ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
l : List (Perm α)
h : f ∈ l
hl : List.Pairwise Disjoint l
⊢ ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((l.prod : (a : α) → α) x : α)
have nil : ∀ (h : Membership.mem (γ := List (Perm α)) [] f) (hl : List.Pairwise.{u_1} (α := Perm α) Disjoint []),
  ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((List.prod [] : (a : α) → α) x : α)
Tactic: induction l with
  | nil => simp at h
  | cons hd tl IH =>
    intro x hx
    rw [List.pairwise_cons] at hl
    rw [List.mem_cons] at h
    rcases h with (rfl | h)
    · rw [List.prod_cons, mul_apply,
        notMem_support.mp ((disjoint_prod_right tl hl.left).mem_imp hx)]
    · rw [List.prod_cons, mul_apply, ← IH h hl.right _ hx, eq_comm, ← notMem_support]
      refine (hl.left _ h).symm.mem_imp ?_
      simpa using hx
Cleared hypotheses: l, h, hl
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
l : List (Perm α)
h : f ∈ l
hl : List.Pairwise Disjoint l
nil :
  ∀ (h : Membership.mem (γ := List (Perm α)) [] f) (hl : List.Pairwise.{u_1} (α := Perm α) Disjoint []),
    ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((List.prod [] : (a : α) → α) x : α)
⊢ ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((l.prod : (a : α) → α) x : α)
have cons : ∀ (hd : Perm α) (tl : List (Perm α))
  (IH :
    ∀ (h : f ∈ tl) (hl : List.Pairwise Disjoint tl),
      ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((tl.prod : (a : α) → α) x : α))
  (h : f ∈ hd :: tl) (hl : List.Pairwise Disjoint (hd :: tl)),
  ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) (((hd :: tl).prod : (a : α) → α) x : α)
Tactic: induction l with
  | nil => simp at h
  | cons hd tl IH =>
    intro x hx
    rw [List.pairwise_cons] at hl
    rw [List.mem_cons] at h
    rcases h with (rfl | h)
    · rw [List.prod_cons, mul_apply,
        notMem_support.mp ((disjoint_prod_right tl hl.left).mem_imp hx)]
    · rw [List.prod_cons, mul_apply, ← IH h hl.right _ hx, eq_comm, ← notMem_support]
      refine (hl.left _ h).symm.mem_imp ?_
      simpa using hx
Cleared hypotheses: l, h, hl
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f g x y : Perm α
h : f.Disjoint g
hf : x.support ≤ f.support
hg : y.support ≤ g.support
⊢ x.Disjoint y
have rw : ∀ (h : _root_.Disjoint f.support g.support) (hf : x.support ≤ f.support) (hg : y.support ≤ g.support),
  _root_.Disjoint x.support y.support
Tactic: rw [disjoint_iff_disjoint_support] at h ⊢
Cleared hypotheses: h, hf, hg
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
l : List (Perm α)
h : f ∈ l
hl : List.Pairwise Disjoint l
x : α
hx : x ∈ f.support
⊢ x ∈ l.prod.support
have rwa : (l.prod : (a : α) → α) x ≠ x
Tactic: rwa [mem_support, ← eq_on_support_mem_disjoint h hl _ hx, ← mem_support]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
l : List (Perm α)
h : f ∈ l
hl : List.Pairwise Disjoint l
x : α
hx : x ∈ f.support
rwa : (l.prod : (a : α) → α) x ≠ x
⊢ x ∈ l.prod.support
have rwa₁ : (f : (a : α) → α) x ≠ x
Tactic: rwa [mem_support, ← eq_on_support_mem_disjoint h hl _ hx, ← mem_support]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
β : Type u_2
inst_2 : DecidableEq β
inst_3 : Fintype β
p : β → Prop
inst_4 : DecidablePred p
f : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α (Subtype p)
g : Perm α
⊢ (g.extendDomain (p := p) f).support = map (f.asEmbedding (p := p)) g.support
have h : ∀ (b : β), b ∈ (g.extendDomain (p := p) f).support ↔ b ∈ map (f.asEmbedding (p := p)) g.support
Tactic: ext b
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
β : Type u_2
inst_2 : DecidableEq β
inst_3 : Fintype β
p : β → Prop
inst_4 : DecidablePred p
f : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α (Subtype p)
g : Perm α
b : β
⊢ b ∈ (g.extendDomain (p := p) f).support ↔ b ∈ map (f.asEmbedding (p := p)) g.support
have h : ¬(g.extendDomain (p := p) f : (a : β) → β) b = b ↔
  ∃ (a : α), ¬(g : (a : α) → α) a = a ∧ (f.asEmbedding (p := p) : (a : α) → β) a = b
Tactic: simp only [mem_map, Ne,
    mem_support]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
β : Type u_2
inst_2 : DecidableEq β
inst_3 : Fintype β
p : β → Prop
inst_4 : DecidablePred p
f : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α (Subtype p)
g : Perm α
b : β
⊢ ¬(g.extendDomain (p := p) f : (a : β) → β) b = b ↔
    ∃ (a : α), ¬(g : (a : α) → α) a = a ∧ (f.asEmbedding (p := p) : (a : α) → β) a = b
have pos : ∀ (pb : p b),
  ¬(g.extendDomain (p := p) f : (a : β) → β) b = b ↔
    ∃ (a : α), ¬(g : (a : α) → α) a = a ∧ (f.asEmbedding (p := p) : (a : α) → β) a = b
Tactic: by_cases pb : p b
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
β : Type u_2
inst_2 : DecidableEq β
inst_3 : Fintype β
p : β → Prop
inst_4 : DecidablePred p
f : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α (Subtype p)
g : Perm α
b : β
pos :
  ∀ (pb : p b),
    ¬(g.extendDomain (p := p) f : (a : β) → β) b = b ↔
      ∃ (a : α), ¬(g : (a : α) → α) a = a ∧ (f.asEmbedding (p := p) : (a : α) → β) a = b
⊢ ¬(g.extendDomain (p := p) f : (a : β) → β) b = b ↔
    ∃ (a : α), ¬(g : (a : α) → α) a = a ∧ (f.asEmbedding (p := p) : (a : α) → β) a = b
have neg : ∀ (pb : ¬p b),
  ¬(g.extendDomain (p := p) f : (a : β) → β) b = b ↔
    ∃ (a : α), ¬(g : (a : α) → α) a = a ∧ (f.asEmbedding (p := p) : (a : α) → β) a = b
Tactic: by_cases pb : p b
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
β : Type u_2
inst_2 : DecidableEq β
inst_3 : Fintype β
p : β → Prop
inst_4 : DecidablePred p
f : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α (Subtype p)
g : Perm α
b : β
pb : p b
⊢ ¬(g.extendDomain (p := p) f : (a : β) → β) b = b ↔
    ∃ (a : α), ¬(g : (a : α) → α) a = a ∧ (f.asEmbedding (p := p) : (a : α) → β) a = b
have pos : ¬(↑((f : (a : α) → Subtype p) ((g : (a : α) → α) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b pb) : α))) :
        β) =
      b ↔
  ∃ (a : α), ¬(g : (a : α) → α) a = a ∧ (f.asEmbedding (p := p) : (a : α) → β) a = b
Tactic: rw [extendDomain_apply_subtype _ _ pb]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
β : Type u_2
inst_2 : DecidableEq β
inst_3 : Fintype β
p : β → Prop
inst_4 : DecidablePred p
f : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α (Subtype p)
g : Perm α
b : β
pb : ¬p b
⊢ ¬(g.extendDomain (p := p) f : (a : β) → β) b = b ↔
    ∃ (a : α), ¬(g : (a : α) → α) a = a ∧ (f.asEmbedding (p := p) : (a : α) → β) a = b
have neg : ¬b = b ↔ ∃ (a : α), ¬(g : (a : α) → α) a = a ∧ (f.asEmbedding (p := p) : (a : α) → β) a = b
Tactic: rw [extendDomain_apply_not_subtype _ _ pb]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
β : Type u_2
inst_2 : DecidableEq β
inst_3 : Fintype β
p : β → Prop
inst_4 : DecidablePred p
f : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α (Subtype p)
g : Perm α
b : β
pb : ¬p b
⊢ ¬b = b ↔ ∃ (a : α), ¬(g : (a : α) → α) a = a ∧ (f.asEmbedding (p := p) : (a : α) → β) a = b
have neg : ∀ (x : α), ¬(g : (a : α) → α) x = x → ¬(f.asEmbedding (p := p) : (a : α) → β) x = b
Tactic: simp only [not_exists, false_iff, not_and, not_true]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
⊢ #f.support = 0 ↔ f = 1
have rw : f.support = ∅ ↔ f = 1
Tactic: rw [Finset.card_eq_zero, support_eq_empty_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
rw : f.support = ∅ ↔ f = 1
⊢ #f.support = 0 ↔ f = 1
have rw₁ : f = 1 ↔ f = 1
Tactic: rw [Finset.card_eq_zero, support_eq_empty_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : f ≠ 1
⊢ 1 < #f.support
have simp_rw : ∃ (a : α) (b : α), ¬((f : (a : α) → α) a = a ∨ (f : (a : α) → α) b = b ∨ a = b)
Tactic: simp_rw [one_lt_card_iff, mem_support, ← not_or]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : f ≠ 1
⊢ ∃ (a : α) (b : α), ¬((f : (a : α) → α) a = a ∨ (f : (a : α) → α) b = b ∨ a = b)
have contrapose! : ∀ (h : ∀ (a b : α), (f : (a : α) → α) a = a ∨ (f : (a : α) → α) b = b ∨ a = b), f = 1
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : ∀ (a b : α), (f : (a : α) → α) a = a ∨ (f : (a : α) → α) b = b ∨ a = b
⊢ f = 1
have H : ∀ (a : α), Eq (α := α) ((f : (a : α) → α) a : α) ((1 : (a : α) → α) a : α)
Tactic: ext a
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : ∀ (a b : α), (f : (a : α) → α) a = a ∨ (f : (a : α) → α) b = b ∨ a = b
a : α
⊢ Eq (α := α) ((f : (a : α) → α) a : α) ((1 : (a : α) → α) a : α)
have h₁ : Eq (α := α) ((f : (a : α) → α) ((f : (a : α) → α) a : α) : α) ((f : (a : α) → α) a : α) ∨
  (f : (a : α) → α) a = a ∨ (f : (a : α) → α) a = a
Tactic: specialize h (f a) a
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
a : α
h :
  Eq (α := α) ((f : (a : α) → α) ((f : (a : α) → α) a : α) : α) ((f : (a : α) → α) a : α) ∨
    (f : (a : α) → α) a = a ∨ (f : (a : α) → α) a = a
⊢ Eq (α := α) ((f : (a : α) → α) a : α) ((1 : (a : α) → α) a : α)
have H : ∀ (h : (f : (a : α) → α) a = a ∨ (f : (a : α) → α) a = a ∨ (f : (a : α) → α) a = a),
  Eq (α := α) ((f : (a : α) → α) a : α) ((1 : (a : α) → α) a : α)
Tactic: rwa [apply_eq_iff_eq, or_self_iff, or_self_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
a : α
h :
  Eq (α := α) ((f : (a : α) → α) ((f : (a : α) → α) a : α) : α) ((f : (a : α) → α) a : α) ∨
    (f : (a : α) → α) a = a ∨ (f : (a : α) → α) a = a
H :
  ∀ (h : (f : (a : α) → α) a = a ∨ (f : (a : α) → α) a = a ∨ (f : (a : α) → α) a = a),
    Eq (α := α) ((f : (a : α) → α) a : α) ((1 : (a : α) → α) a : α)
⊢ Eq (α := α) ((f : (a : α) → α) a : α) ((1 : (a : α) → α) a : α)
have H₁ : ∀ (h : (f : (a : α) → α) a = a ∨ (f : (a : α) → α) a = a),
  Eq (α := α) ((f : (a : α) → α) a : α) ((1 : (a : α) → α) a : α)
Tactic: rwa [apply_eq_iff_eq, or_self_iff, or_self_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
a : α
h :
  Eq (α := α) ((f : (a : α) → α) ((f : (a : α) → α) a : α) : α) ((f : (a : α) → α) a : α) ∨
    (f : (a : α) → α) a = a ∨ (f : (a : α) → α) a = a
H :
  ∀ (h : (f : (a : α) → α) a = a ∨ (f : (a : α) → α) a = a ∨ (f : (a : α) → α) a = a),
    Eq (α := α) ((f : (a : α) → α) a : α) ((1 : (a : α) → α) a : α)
H₁ :
  ∀ (h : (f : (a : α) → α) a = a ∨ (f : (a : α) → α) a = a),
    Eq (α := α) ((f : (a : α) → α) a : α) ((1 : (a : α) → α) a : α)
⊢ Eq (α := α) ((f : (a : α) → α) a : α) ((1 : (a : α) → α) a : α)
have H₂ : ∀ (h : (f : (a : α) → α) a = a), Eq (α := α) ((f : (a : α) → α) a : α) ((1 : (a : α) → α) a : α)
Tactic: rwa [apply_eq_iff_eq, or_self_iff, or_self_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
⊢ #f.support ≠ 1
have pos : ∀ (h : f = 1), #f.support ≠ 1
Tactic: by_cases h : f = 1
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
pos : ∀ (h : f = 1), #f.support ≠ 1
⊢ #f.support ≠ 1
have neg : ∀ (h : ¬f = 1), #f.support ≠ 1
Tactic: by_cases h : f = 1
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
⊢ #f.support ≤ 1 ↔ f = 1
have rw : #f.support < 1 ∨ #f.support = 1 ↔ f = 1
Tactic: rw [le_iff_lt_or_eq, Nat.lt_succ_iff, Nat.le_zero, card_support_eq_zero, or_iff_not_imp_right,
    imp_iff_right f.card_support_ne_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
rw : #f.support < 1 ∨ #f.support = 1 ↔ f = 1
⊢ #f.support ≤ 1 ↔ f = 1
have rw₁ : #f.support ≤ 0 ∨ #f.support = 1 ↔ f = 1
Tactic: rw [le_iff_lt_or_eq, Nat.lt_succ_iff, Nat.le_zero, card_support_eq_zero, or_iff_not_imp_right,
    imp_iff_right f.card_support_ne_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
rw : #f.support < 1 ∨ #f.support = 1 ↔ f = 1
rw₁ : #f.support ≤ 0 ∨ #f.support = 1 ↔ f = 1
⊢ #f.support ≤ 1 ↔ f = 1
have rw₂ : #f.support = 0 ∨ #f.support = 1 ↔ f = 1
Tactic: rw [le_iff_lt_or_eq, Nat.lt_succ_iff, Nat.le_zero, card_support_eq_zero, or_iff_not_imp_right,
    imp_iff_right f.card_support_ne_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
rw : #f.support < 1 ∨ #f.support = 1 ↔ f = 1
rw₁ : #f.support ≤ 0 ∨ #f.support = 1 ↔ f = 1
rw₂ : #f.support = 0 ∨ #f.support = 1 ↔ f = 1
⊢ #f.support ≤ 1 ↔ f = 1
have rw₃ : f = 1 ∨ #f.support = 1 ↔ f = 1
Tactic: rw [le_iff_lt_or_eq, Nat.lt_succ_iff, Nat.le_zero, card_support_eq_zero, or_iff_not_imp_right,
    imp_iff_right f.card_support_ne_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
rw : #f.support < 1 ∨ #f.support = 1 ↔ f = 1
rw₁ : #f.support ≤ 0 ∨ #f.support = 1 ↔ f = 1
rw₂ : #f.support = 0 ∨ #f.support = 1 ↔ f = 1
rw₃ : f = 1 ∨ #f.support = 1 ↔ f = 1
⊢ #f.support ≤ 1 ↔ f = 1
have rw₄ : ¬#f.support = 1 → f = 1 ↔ f = 1
Tactic: rw [le_iff_lt_or_eq, Nat.lt_succ_iff, Nat.le_zero, card_support_eq_zero, or_iff_not_imp_right,
    imp_iff_right f.card_support_ne_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
rw : #f.support < 1 ∨ #f.support = 1 ↔ f = 1
rw₁ : #f.support ≤ 0 ∨ #f.support = 1 ↔ f = 1
rw₂ : #f.support = 0 ∨ #f.support = 1 ↔ f = 1
rw₃ : f = 1 ∨ #f.support = 1 ↔ f = 1
rw₄ : ¬#f.support = 1 → f = 1 ↔ f = 1
⊢ #f.support ≤ 1 ↔ f = 1
have rw₅ : f = 1 ↔ f = 1
Tactic: rw [le_iff_lt_or_eq, Nat.lt_succ_iff, Nat.le_zero, card_support_eq_zero, or_iff_not_imp_right,
    imp_iff_right f.card_support_ne_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
⊢ #f.support = 2 ↔ f.IsSwap
have mp : #f.support = 2 → f.IsSwap
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
mp : #f.support = 2 → f.IsSwap
⊢ #f.support = 2 ↔ f.IsSwap
have mpr : f.IsSwap → #f.support = 2
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : #f.support = 2
⊢ f.IsSwap
have mp : ∀ (x : α) (t : Finset α) (hmem : x ∉ t) (hins : insert x t = f.support) (ht : #t = 1), f.IsSwap
Tactic: obtain ⟨x, t, hmem, hins, ht⟩ := card_eq_succ.1 h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : #f.support = 2
x : α
t : Finset α
hmem : x ∉ t
hins : insert x t = f.support
ht : #t = 1
⊢ f.IsSwap
have mp : ∀ (y : α) (hmem : x ∉ {y}) (hins : {x, y} = f.support) (ht : card (α := α) {y} = 1), f.IsSwap
Tactic: obtain ⟨y, rfl⟩ := card_eq_one.1 ht
Cleared hypotheses: t, hmem, hins, ht
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : x ∉ {y}
hins : {x, y} = f.support
ht : card (α := α) {y} = 1
⊢ f.IsSwap
have hmem₁ : ¬x = y
Tactic: rw [mem_singleton] at hmem
Cleared hypotheses: hmem, hins, ht
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : ¬x = y
hins : {x, y} = f.support
ht : card (α := α) {y} = 1
⊢ f.IsSwap
have mp : f = swap x y
Tactic: refine ⟨x, y, hmem, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : ¬x = y
hins : {x, y} = f.support
ht : card (α := α) {y} = 1
⊢ f = swap x y
have mp : ∀ (a : α), Eq (α := α) ((f : (a : α) → α) a : α) ((swap x y : (a : α) → α) a : α)
Tactic: ext a
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : ¬x = y
hins : {x, y} = f.support
ht : card (α := α) {y} = 1
a b : α
⊢ (f : (a : α) → α) b ≠ b ↔ b = x ∨ b = y
have rw : b ∈ f.support ↔ b = x ∨ b = y
Tactic: rw [← mem_support, ← hins, mem_insert, mem_singleton]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : ¬x = y
hins : {x, y} = f.support
ht : card (α := α) {y} = 1
a b : α
rw : b ∈ f.support ↔ b = x ∨ b = y
⊢ (f : (a : α) → α) b ≠ b ↔ b = x ∨ b = y
have rw₁ : Membership.mem (γ := Finset α) {x, y} b ↔ b = x ∨ b = y
Tactic: rw [← mem_support, ← hins, mem_insert, mem_singleton]