awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Support
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
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
⊢ ¬(g.extendDomain (p := p) f : (a : β) → β) b = b ↔
    ∃ (a : α), ¬(g : (a : α) → α) a = a ∧ (f.asEmbedding (p := p) : (a : α) → β) a = b

Tactic:
rw [extendDomain_apply_subtype _ _ pb]

Premises used: Equiv.Perm.extendDomain_apply_subtype
-- Module: Mathlib.GroupTheory.Perm.Support
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
⊢ ¬(↑((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:
grind [asEmbedding_apply]

Premises used: Equiv.asEmbedding_apply
-- Module: Mathlib.GroupTheory.Perm.Support
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
neg : ¬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

Tactic:
rw [extendDomain_apply_not_subtype _ _ pb]

Premises used: Equiv.Perm.extendDomain_apply_not_subtype
-- Module: Mathlib.GroupTheory.Perm.Support
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
neg : ∀ (x : α), ¬(g : (a : α) → α) x = x → ¬(f.asEmbedding (p := p) : (a : α) → β) x = b
⊢ ¬b = b ↔ ∃ (a : α), ¬(g : (a : α) → α) a = a ∧ (f.asEmbedding (p := p) : (a : α) → β) a = b

Tactic:
simp only [not_exists, false_iff, not_and, not_true]

Premises used: not_exists, false_iff, not_true, not_and
-- Module: Mathlib.GroupTheory.Perm.Support
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 α
a : α
h : ¬(g : (a : α) → α) a = a
pb : ¬p ((f.asEmbedding (p := p) : (a : α) → β) a)
⊢ False

Tactic:
pb (Subtype.prop _)

Premises used: Subtype.prop
-- Module: Mathlib.GroupTheory.Perm.Support
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 α
a : α
h : ¬(g : (a : α) → α) a = a
pb : ¬p ((f.asEmbedding (p := p) : (a : α) → β) a)
⊢ False

Tactic:
exact pb (Subtype.prop _)

Premises used: Subtype.prop
-- Module: Mathlib.GroupTheory.Perm.Support
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 = #g.support

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
rw : f.support = ∅ ↔ f = 1
rw₁ rw₂ : f = 1 ↔ f = 1
⊢ #f.support = 0 ↔ f = 1

Tactic:
rw [Finset.card_eq_zero, support_eq_empty_iff]

Premises used: Equiv.Perm.support_eq_empty_iff, Finset.card_eq_zero
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : f ≠ 1
simp_rw : ∃ (a : α) (b : α), ¬((f : (a : α) → α) a = a ∨ (f : (a : α) → α) b = b ∨ a = b)
⊢ 1 < #f.support

Tactic:
simp_rw [one_lt_card_iff, mem_support, ← not_or]

Premises used: Equiv.Perm.mem_support, Finset.one_lt_card_iff, not_or
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : f ≠ 1
contrapose! : ∀ (h : ∀ (a b : α), (f : (a : α) → α) a = a ∨ (f : (a : α) → α) b = b ∨ a = b), f = 1
⊢ ∃ (a : α) (b : α), ¬((f : (a : α) → α) a = a ∨ (f : (a : α) → α) b = b ∨ a = b)

Tactic:
contrapose! h
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : ∀ (a b : α), (f : (a : α) → α) a = a ∨ (f : (a : α) → α) b = b ∨ a = b
H : ∀ (a : α), Eq (α := α) ((f : (a : α) → α) a : α) ((1 : (a : α) → α) a : α)
⊢ f = 1

Tactic:
ext a
-- Module: Mathlib.GroupTheory.Perm.Support
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 : α) → α) ((f : (a : α) → α) a : α) : α) ((f : (a : α) → α) a : α) ∨
    (f : (a : α) → α) a = a ∨ (f : (a : α) → α) a = a

Tactic:
specialize h (f a) a

Premises used: DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.Support
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 : α)
H₂ H₃ H₄ H₅ : ∀ (h : (f : (a : α) → α) a = a), Eq (α := α) ((f : (a : α) → α) a : α) ((1 : (a : α) → α) a : α)
⊢ Eq (α := α) ((f : (a : α) → α) a : α) ((1 : (a : α) → α) a : α)

Tactic:
rwa [apply_eq_iff_eq, or_self_iff, or_self_iff] at h

Premises used: or_self_iff, Equiv.apply_eq_iff_eq
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
pos : ∀ (h : f = 1), #f.support ≠ 1
neg : ∀ (h : ¬f = 1), #f.support ≠ 1
⊢ #f.support ≠ 1

Tactic:
by_cases h : f = 1
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : f = 1
⊢ #f.support ≠ 1

Tactic:
ne_of_eq_of_ne (card_support_eq_zero.mpr h) zero_ne_one

Premises used: Iff.mpr, ne_of_eq_of_ne, Equiv.Perm.card_support_eq_zero, zero_ne_one
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : f = 1
⊢ #f.support ≠ 1

Tactic:
exact ne_of_eq_of_ne (card_support_eq_zero.mpr h) zero_ne_one

Premises used: Iff.mpr, ne_of_eq_of_ne, Equiv.Perm.card_support_eq_zero, zero_ne_one
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : ¬f = 1
⊢ #f.support ≠ 1

Tactic:
ne_of_gt (one_lt_card_support_of_ne_one h)

Premises used: ne_of_gt, Equiv.Perm.one_lt_card_support_of_ne_one
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : ¬f = 1
⊢ #f.support ≠ 1

Tactic:
exact ne_of_gt (one_lt_card_support_of_ne_one h)

Premises used: ne_of_gt, Equiv.Perm.one_lt_card_support_of_ne_one
-- Module: Mathlib.GroupTheory.Perm.Support
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
rw₅ rw₆ : f = 1 ↔ 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]

Premises used: Classical.or_iff_not_imp_right, Equiv.Perm.card_support_ne_one, Equiv.Perm.card_support_eq_zero, Nat.le_zero, imp_iff_right, le_iff_lt_or_eq, Nat.lt_succ_iff
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : f ≠ 1
⊢ 2 ≤ #f.support

Tactic:
one_lt_card_support_of_ne_one h

Premises used: Equiv.Perm.one_lt_card_support_of_ne_one, Nat.lt
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x : α
hx : (f : (a : α) → α) x ≠ x
h : f.support ⊆ (swap x ((f : (a : α) → α) x) * f).support
⊢ ¬(swap x ((f : (a : α) → α) x) * f : (a : α) → α) x ≠ x

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
x y : α
hxy : x ≠ y
⊢ (x ::ₘ y ::ₘ 0).Nodup

Tactic:
simp [hxy]
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
x y : α
hxy : x ≠ y
⊢ (swap x y).support = { val := x ::ₘ y ::ₘ 0, nodup := ⋯ }

Tactic:
simp [support_swap hxy, *, Finset.ext_iff]

Premises used: Finset.ext_iff, Equiv.Perm.support_swap
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
mp : #f.support = 2 → f.IsSwap
mpr : f.IsSwap → #f.support = 2
⊢ #f.support = 2 ↔ f.IsSwap

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : #f.support = 2
mp : ∀ (x : α) (t : Finset α) (hmem : x ∉ t) (hins : insert x t = f.support) (ht : #t = 1), f.IsSwap
⊢ f.IsSwap

Tactic:
obtain ⟨x, t, hmem, hins, ht⟩ := card_eq_succ.1 h

Premises used: Finset.card_eq_succ, Iff.mp
-- Module: Mathlib.GroupTheory.Perm.Support
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
mp : ∀ (y : α) (hmem : x ∉ {y}) (hins : {x, y} = f.support) (ht : card (α := α) {y} = 1), f.IsSwap
⊢ f.IsSwap

Tactic:
obtain ⟨y, rfl⟩ := card_eq_one.1 ht

Premises used: Finset.card_eq_one, Iff.mp, rfl
-- Module: Mathlib.GroupTheory.Perm.Support
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
⊢ ¬x = y

Tactic:
rw [mem_singleton] at hmem

Premises used: Finset.mem_singleton
-- Module: Mathlib.GroupTheory.Perm.Support
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
hmem₁ : ¬x = y
⊢ {x, y} = f.support

Tactic:
rw [mem_singleton] at hmem

Premises used: Finset.mem_singleton
-- Module: Mathlib.GroupTheory.Perm.Support
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
hmem₁ : ¬x = y
hins₁ : {x, y} = f.support
⊢ card (α := α) {y} = 1

Tactic:
rw [mem_singleton] at hmem

Premises used: Finset.mem_singleton
-- Module: Mathlib.GroupTheory.Perm.Support
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

Tactic:
⟨x, y, hmem, ?_⟩

Premises used: Equiv.Perm.IsSwap, And.intro, Exists.intro
-- Module: Mathlib.GroupTheory.Perm.Support
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
mp : f = swap x y
⊢ f.IsSwap

Tactic:
refine ⟨x, y, hmem, ?_⟩
-- Module: Mathlib.GroupTheory.Perm.Support
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
mp : ∀ (a : α), Eq (α := α) ((f : (a : α) → α) a : α) ((swap x y : (a : α) → α) a : α)
⊢ f = swap x y

Tactic:
ext a
-- Module: Mathlib.GroupTheory.Perm.Support
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
rw₁ : Membership.mem (γ := Finset α) {x, y} b ↔ b = x ∨ b = y
rw₂ : b = x ∨ Membership.mem (γ := Finset α) {y} b ↔ b = x ∨ b = y
rw₃ rw₄ : b = x ∨ b = y ↔ b = x ∨ b = y
⊢ (f : (a : α) → α) b ≠ b ↔ b = x ∨ b = y

Tactic:
rw [← mem_support, ← hins, mem_insert, mem_singleton]

Premises used: Finset.mem_singleton, Equiv.Perm.mem_support, Finset.mem_insert
-- Module: Mathlib.GroupTheory.Perm.Support
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

Tactic:
have key : ∀ b, f b ≠ b ↔ _ := fun b => by rw [← mem_support, ← hins, mem_insert, mem_singleton]
-- Module: Mathlib.GroupTheory.Perm.Support
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 : α
key : ∀ (b : α), (f : (a : α) → α) b ≠ b ↔ b = x ∨ b = y
pos : ∀ (ha : (f : (a : α) → α) a = a), Eq (α := α) ((f : (a : α) → α) a : α) ((swap x y : (a : α) → α) a : α)
neg : ∀ (ha : ¬(f : (a : α) → α) a = a), Eq (α := α) ((f : (a : α) → α) a : α) ((swap x y : (a : α) → α) a : α)
⊢ Eq (α := α) ((f : (a : α) → α) a : α) ((swap x y : (a : α) → α) a : α)

Tactic:
by_cases ha : f a = a

Premises used: DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.Support
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 : α
key : ∀ (b : α), (f : (a : α) → α) b ≠ b ↔ b = x ∨ b = y
ha : (f : (a : α) → α) a = a
⊢ ¬a = x ∧ ¬a = y

Tactic:
have ha' := not_or.mp (mt (key a).mpr (not_not.mpr ha))
-- Module: Mathlib.GroupTheory.Perm.Support
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 : α
key : ∀ (b : α), (f : (a : α) → α) b ≠ b ↔ b = x ∨ b = y
ha : (f : (a : α) → α) a = a
ha' : ¬a = x ∧ ¬a = y
pos : a = (swap x y : (a : α) → α) a
pos₁ pos₂ : a = a
⊢ Eq (α := α) ((f : (a : α) → α) a : α) ((swap x y : (a : α) → α) a : α)

Tactic:
rw [ha, swap_apply_of_ne_of_ne ha'.1 ha'.2]

Premises used: Equiv.swap_apply_of_ne_of_ne, And.right, And.left
-- Module: Mathlib.GroupTheory.Perm.Support
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 : α
key : ∀ (b : α), (f : (a : α) → α) b ≠ b ↔ b = x ∨ b = y
ha : ¬(f : (a : α) → α) a = a
⊢ (f : (a : α) → α) a = x ∨ (f : (a : α) → α) a = y

Tactic:
have ha' := (key (f a)).mp (mt f.apply_eq_iff_eq.mp ha)
-- Module: Mathlib.GroupTheory.Perm.Support
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 : α
key : ∀ (b : α), (f : (a : α) → α) b ≠ b ↔ b = x ∨ b = y
ha : ¬(f : (a : α) → α) a = a
ha' : (f : (a : α) → α) a = x ∨ (f : (a : α) → α) a = y
neg :
  ∀ (hmem : ¬a = y) (hins : {a, y} = f.support) (key : ∀ (b : α), (f : (a : α) → α) b ≠ b ↔ b = a ∨ b = y)
    (ha' : (f : (a : α) → α) a = a ∨ (f : (a : α) → α) a = y),
    Eq (α := α) ((f : (a : α) → α) a : α) ((swap a y : (a : α) → α) a : α)
neg₁ :
  ∀ (hmem : ¬x = a) (hins : {x, a} = f.support) (ht : card (α := α) {a} = 1)
    (key : ∀ (b : α), (f : (a : α) → α) b ≠ b ↔ b = x ∨ b = a)
    (ha' : (f : (a : α) → α) a = x ∨ (f : (a : α) → α) a = a),
    Eq (α := α) ((f : (a : α) → α) a : α) ((swap x a : (a : α) → α) a : α)
⊢ Eq (α := α) ((f : (a : α) → α) a : α) ((swap x y : (a : α) → α) a : α)

Tactic:
obtain rfl | rfl := (key a).mp ha

Premises used: Iff.mp, rfl
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : #f.support = 2
y : α
ht : card (α := α) {y} = 1
a : α
ha : ¬(f : (a : α) → α) a = a
hmem : ¬a = y
hins : {a, y} = f.support
key : ∀ (b : α), (f : (a : α) → α) b ≠ b ↔ b = a ∨ b = y
ha' : (f : (a : α) → α) a = a ∨ (f : (a : α) → α) a = y
neg : y = (swap a y : (a : α) → α) a
neg₁ neg₂ : y = y
⊢ Eq (α := α) ((f : (a : α) → α) a : α) ((swap a y : (a : α) → α) a : α)

Tactic:
rw [Or.resolve_left ha' ha, swap_apply_left]

Premises used: Or.resolve_left, Equiv.swap_apply_left
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : #f.support = 2
x a : α
ha : ¬(f : (a : α) → α) a = a
hmem : ¬x = a
hins : {x, a} = f.support
ht : card (α := α) {a} = 1
key : ∀ (b : α), (f : (a : α) → α) b ≠ b ↔ b = x ∨ b = a
ha' : (f : (a : α) → α) a = x ∨ (f : (a : α) → α) a = a
neg : x = (swap x a : (a : α) → α) a
neg₁ neg₂ : x = x
⊢ Eq (α := α) ((f : (a : α) → α) a : α) ((swap x a : (a : α) → α) a : α)

Tactic:
rw [Or.resolve_right ha' ha, swap_apply_right]

Premises used: Or.resolve_right, Equiv.swap_apply_right
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : f.IsSwap
mpr : ∀ (x y : α) (hxy : x ≠ y), #(swap x y).support = 2
⊢ #f.support = 2

Tactic:
obtain ⟨x, y, hxy, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
x y : α
hxy : x ≠ y
⊢ #(swap x y).support = 2

Tactic:
card_support_swap hxy

Premises used: Equiv.Perm.card_support_swap
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
x y : α
hxy : x ≠ y
⊢ #(swap x y).support = 2

Tactic:
exact card_support_swap hxy

Premises used: Equiv.Perm.card_support_swap
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f.Disjoint g
rw : #(f * g).support = #(f.support ∪ g.support)
rw₁ : _root_.Disjoint f.support g.support
⊢ #(f * g).support = #f.support + #g.support

Tactic:
rw [← Finset.card_union_of_disjoint]

Premises used: Finset.card_union_of_disjoint
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f.Disjoint g
e_s : (f * g).support = f.support ∪ g.support
⊢ #(f * g).support = #(f.support ∪ g.support)

Tactic:
congr
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f.Disjoint g
e_s : ∀ (a : α), a ∈ (f * g).support ↔ a ∈ f.support ∪ g.support
⊢ (f * g).support = f.support ∪ g.support

Tactic:
ext
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f.Disjoint g
a : α
⊢ a ∈ (f * g).support ↔ a ∈ f.support ∪ g.support

Tactic:
simp [h.support_mul]

Premises used: Equiv.Perm.Disjoint.support_mul
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ _root_.Disjoint f.support g.support

Tactic:
simpa using h.disjoint_support

Premises used: Equiv.Perm.Disjoint.disjoint_support
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
h : List.Pairwise.{u_1} (α := Perm α) Disjoint []
⊢ card.{u_1} (α := α) (support (List.prod [])) = (List.map.{u_1, 0} (α := Perm α) (card ∘ support) []).sum

Tactic:
card_support_eq_zero.mpr rfl

Premises used: Iff.mpr, Equiv.Perm.card_support_eq_zero, List.sum, List.foldr, rfl
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
h : List.Pairwise.{u_1} (α := Perm α) Disjoint []
⊢ card.{u_1} (α := α) (support (List.prod [])) = (List.map.{u_1, 0} (α := Perm α) (card ∘ support) []).sum

Tactic:
exact card_support_eq_zero.mpr rfl

Premises used: Iff.mpr, Equiv.Perm.card_support_eq_zero, rfl
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
a : Perm α
t : List (Perm α)
ih : ∀ (h : List.Pairwise Disjoint t), #t.prod.support = (List.map (card ∘ support) t).sum
h : List.Pairwise Disjoint (a :: t)
⊢ ∀ a' ∈ t, a.Disjoint a'

Tactic:
obtain ⟨ha, ht⟩ := List.pairwise_cons.1 h

Premises used: List.pairwise_cons, Iff.mp
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
a : Perm α
t : List (Perm α)
ih : ∀ (h : List.Pairwise Disjoint t), #t.prod.support = (List.map (card ∘ support) t).sum
h : List.Pairwise Disjoint (a :: t)
ha : ∀ a' ∈ t, a.Disjoint a'
⊢ List.Pairwise Disjoint t

Tactic:
obtain ⟨ha, ht⟩ := List.pairwise_cons.1 h

Premises used: List.pairwise_cons, Iff.mp
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
a : Perm α
t : List (Perm α)
ih : ∀ (h : List.Pairwise Disjoint t), #t.prod.support = (List.map (card ∘ support) t).sum
h : List.Pairwise Disjoint (a :: t)
ha : ∀ a' ∈ t, a.Disjoint a'
ht : List.Pairwise Disjoint t
cons : #(a * t.prod).support = (card ∘ support) a + #t.prod.support
⊢ #(a :: t).prod.support = (List.map (card ∘ support) (a :: t)).sum

Tactic:
rw [List.prod_cons, List.map_cons, List.sum_cons, ← ih ht]

Premises used: List.map_cons, List.sum_cons, List.prod_cons
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
a : Perm α
t : List (Perm α)
ih : ∀ (h : List.Pairwise Disjoint t), #t.prod.support = (List.map (card ∘ support) t).sum
h : List.Pairwise Disjoint (a :: t)
ha : ∀ a' ∈ t, a.Disjoint a'
ht : List.Pairwise Disjoint t
⊢ #(a * t.prod).support = (card ∘ support) a + #t.prod.support

Tactic:
(disjoint_prod_right _ ha).card_support_mul

Premises used: Equiv.Perm.Disjoint.card_support_mul, Equiv.Perm.disjoint_prod_right, Finset.card, Multiset.card
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
a : Perm α
t : List (Perm α)
ih : ∀ (h : List.Pairwise Disjoint t), #t.prod.support = (List.map (card ∘ support) t).sum
h : List.Pairwise Disjoint (a :: t)
ha : ∀ a' ∈ t, a.Disjoint a'
ht : List.Pairwise Disjoint t
⊢ #(a * t.prod).support = (card ∘ support) a + #t.prod.support

Tactic:
exact (disjoint_prod_right _ ha).card_support_mul

Premises used: Equiv.Perm.Disjoint.card_support_mul, Equiv.Perm.disjoint_prod_right
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
l : List (Perm α)
h : List.Pairwise Disjoint l
nil :
  ∀ (h : List.Pairwise.{u_1} (α := Perm α) Disjoint []),
    card.{u_1} (α := α) (support (List.prod [])) = (List.map.{u_1, 0} (α := Perm α) (card ∘ support) []).sum
cons :
  ∀ (a : Perm α) (t : List (Perm α))
    (ih : ∀ (h : List.Pairwise Disjoint t), #t.prod.support = (List.map (card ∘ support) t).sum)
    (h : List.Pairwise Disjoint (a :: t)), #(a :: t).prod.support = (List.map (card ∘ support) (a :: t)).sum
⊢ #l.prod.support = (List.map (card ∘ support) l).sum

Tactic:
induction l with
  | nil => exact card_support_eq_zero.mpr rfl
  | cons a t ih =>
    obtain ⟨ha, ht⟩ := List.pairwise_cons.1 h
    rw [List.prod_cons, List.map_cons, List.sum_cons, ← ih ht]
    exact (disjoint_prod_right _ ha).card_support_mul

Premises used: Iff.mpr, List.map_cons, Equiv.Perm.card_support_eq_zero, Finset.cons, List.pairwise_cons, List.sum_cons, Iff.mp, List.prod_cons, rfl
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
f : Perm α
h : ∀ (x : α), Membership.mem (α := α) s ((f : (a : α) → α) x : α) ↔ x ∈ s
h₁ :
  ∀ (a : ↥s),
    a ∈ (f.subtypePerm (p := Membership.mem s) h).support ↔
      Membership.mem (γ := Finset ↥s) {x : ↥s | (f : (a : α) → α) (↑x : α) ≠ (↑x : α)} a
⊢ (f.subtypePerm (p := Membership.mem s) h).support = {x : ↥s | (f : (a : α) → α) (↑x : α) ≠ (↑x : α)}

Tactic:
ext