awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
σa : Perm α
σb : Perm β
this :
  Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr 1) : ℤˣ)
      (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa : ℤˣ) ∧
    Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 σb) : ℤˣ)
      (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb : ℤˣ)
rw :
  ((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr σb) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr 1) : ℤˣ)
      (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb : ℤˣ)
rw₁ :
  ((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr σb) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr 1) : ℤˣ)
      (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 σb) : ℤˣ)
rw₂ :
  Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr σb) : ℤˣ)
    (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr 1 * sumCongr 1 σb) : ℤˣ)
rw₃ :
  Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr σb) : ℤˣ)
    (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) ((σa * 1).sumCongr (1 * σb)) : ℤˣ)
rw₄ :
  Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr σb) : ℤˣ)
    (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) ((σa * 1).sumCongr σb) : ℤˣ)
rw₅ rw₆ :
  Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr σb) : ℤˣ)
    (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr σb) : ℤˣ)
⊢ ((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr σb) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa : ℤˣ)
      (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb : ℤˣ)

Tactic:
rw [← this.1, ← this.2, ← sign_mul, sumCongr_mul, one_mul, mul_one]

Premises used: Equiv.Perm.sign_mul, Equiv.Perm.sumCongr_mul, And.right, And.left, mul_one, one_mul
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
σa : Perm α
σb : Perm β
suffices :
  Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr 1) : ℤˣ)
      (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa : ℤˣ) ∧
    Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 σb) : ℤˣ)
      (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb : ℤˣ)
⊢ ((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr σb) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa : ℤˣ)
      (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb : ℤˣ)

Tactic:
suffices sign (sumCongr σa (1 : Perm β)) = sign σa ∧ sign (sumCongr (1 : Perm α) σb) = sign σb
    by rw [← this.1, ← this.2, ← sign_mul, sumCongr_mul, one_mul, mul_one]
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
σa : Perm α
σb : Perm β
left :
  Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr 1) : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa : ℤˣ)
right :
  Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 σb) : ℤˣ)
    (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb : ℤˣ)
⊢ Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr 1) : ℤˣ)
      (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa : ℤˣ) ∧
    Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 σb) : ℤˣ)
      (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb : ℤˣ)

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
σb : Perm β
⊢ Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 1) : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) 1 : ℤˣ)

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
σa : Perm α
σb : Perm β
left :
  Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 1) : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) 1 : ℤˣ)
left₁ :
  ∀ (σa' : Perm α) (a₁ a₂ : α) (ha : a₁ ≠ a₂)
    (ih :
      Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa'.sumCongr 1) : ℤˣ)
        (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa' : ℤˣ)),
    Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) ((swap a₁ a₂ * σa').sumCongr 1) : ℤˣ)
      (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap a₁ a₂ * σa') : ℤˣ)
⊢ Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr 1) : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa : ℤˣ)

Tactic:
induction σa using swap_induction_on with
    | one => simp
    | swap_mul σa' a₁ a₂ ha ih =>
      rw [← one_mul (1 : Perm β), ← sumCongr_mul, sign_mul, sign_mul, ih, sumCongr_swap_one,
        sign_swap ha, sign_swap (Sum.inl_injective.ne_iff.mpr ha)]

Premises used: Equiv.Perm.sign_mul, Equiv.Perm.sumCongr_swap_one, Equiv.Perm.sumCongr_mul, OfNat.ofNat, one_mul
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
σa : Perm α
⊢ Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 1) : ℤˣ)
    (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) 1 : ℤˣ)

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
σa : Perm α
σb : Perm β
right :
  Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 1) : ℤˣ)
    (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) 1 : ℤˣ)
right₁ :
  ∀ (σb' : Perm β) (b₁ b₂ : β) (hb : b₁ ≠ b₂)
    (ih :
      Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 σb') : ℤˣ)
        (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb' : ℤˣ)),
    Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 (swap b₁ b₂ * σb')) : ℤˣ)
      (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (swap b₁ b₂ * σb') : ℤˣ)
⊢ Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 σb) : ℤˣ)
    (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb : ℤˣ)

Tactic:
induction σb using swap_induction_on with
    | one => simp
    | swap_mul σb' b₁ b₂ hb ih =>
      rw [← one_mul (1 : Perm α), ← sumCongr_mul, sign_mul, sign_mul, ih, sumCongr_one_swap,
        sign_swap hb, sign_swap (Sum.inr_injective.ne_iff.mpr hb)]

Premises used: Equiv.Perm.sign_mul, Equiv.Perm.sumCongr_one_swap, Equiv.Perm.sumCongr_mul, OfNat.ofNat, one_mul
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
p : α → Prop
inst_2 : DecidablePred p
ep : Perm { a : α // p a }
en : Perm { a : α // ¬p a }
⊢ ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (ep.subtypeCongr (p := p) en) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm { a : α // p a } →* ℤˣ) : (a : Perm { a : α // p a }) → ℤˣ) ep : ℤˣ)
      (((sign : Perm { a : α // ¬p a } →* ℤˣ) : (a : Perm { a : α // ¬p a }) → ℤˣ) en : ℤˣ)

Tactic:
simp [subtypeCongr]

Premises used: Equiv.Perm.subtypeCongr
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
e : Perm α
p : β → Prop
inst_4 : DecidablePred p
f : Equiv.{u + 1, max 1 (v + 1)} α (Subtype p)
⊢ Eq (α := ℤˣ) (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (e.extendDomain (p := p) f) : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) e : ℤˣ)

Tactic:
simp only [Equiv.Perm.extendDomain, sign_subtypeCongr, sign_permCongr, sign_refl, mul_one]

Premises used: Equiv.Perm.extendDomain, Equiv.Perm.sign_refl, Equiv.Perm.sign_permCongr, mul_one, Equiv.Perm.sign_subtypeCongr
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
p : α → Prop
inst_2 : DecidablePred p
inst_3 : Fintype (Subtype p)
f : Perm (Subtype p)
⊢ Eq (α := ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) ((ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) f) : ℤˣ)
    (((sign : Perm (Subtype p) →* ℤˣ) : (a : Perm (Subtype p)) → ℤˣ) f : ℤˣ)

Tactic:
sign_extendDomain f (Equiv.refl (Subtype p))

Premises used: Equiv.Perm.extendDomain, Subtype, Equiv.Perm.sign_extendDomain, Equiv.Perm.subtypeCongr, Equiv.refl
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : Fintype β
inst_3 : DecidableEq β
e : Perm α
f : α ↪ β
⊢ Eq (α := ℤˣ) (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (e.viaFintypeEmbedding f) : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) e : ℤˣ)

Tactic:
simp [viaFintypeEmbedding]

Premises used: Equiv.Perm.viaFintypeEmbedding
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
s : ℤˣ
σ : Perm α
rw :
  Membership.mem (γ := Finset (Perm α)) {x : Perm α | ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) x = s} σ ↔
    ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ = s
rw₁ :
  Membership.mem (γ := Finset (Perm α)) univ σ ∧ ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ = s ↔
    ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ = s
rw₂ rw₃ : ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ = s ↔ ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ = s
⊢ Membership.mem (γ := Finset (Perm α)) (ofSign s) σ ↔ ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ = s

Tactic:
rw [ofSign, mem_filter, and_iff_right (mem_univ σ)]

Premises used: Finset.mem_univ, and_iff_right, Finset.mem_filter, Equiv.Perm.ofSign
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
rw :
  ∀ (a : Perm α),
    Membership.mem (γ := Finset (Perm α)) (ofSign 1) a →
      ∀ (b : Perm α), Membership.mem (γ := Finset (Perm α)) (ofSign (-1)) b → a ≠ b
⊢ _root_.Disjoint.{u} (α := Finset (Perm α)) (ofSign 1) (ofSign (-1))

Tactic:
rw [Finset.disjoint_iff_ne]

Premises used: Finset.disjoint_iff_ne
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
hσ : Membership.mem (γ := Finset (Perm α)) (ofSign 1) σ
hτ : Membership.mem (γ := Finset (Perm α)) (ofSign (-1)) σ
⊢ Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ : ℤˣ) (1 : ℤˣ)

Tactic:
rw [mem_ofSign] at hσ hτ

Premises used: Equiv.Perm.mem_ofSign
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
hσ : Membership.mem (γ := Finset (Perm α)) (ofSign 1) σ
hτ : Membership.mem (γ := Finset (Perm α)) (ofSign (-1)) σ
hσ₁ : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ : ℤˣ) (1 : ℤˣ)
⊢ Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ : ℤˣ) (-1 : ℤˣ)

Tactic:
rw [mem_ofSign] at hσ hτ

Premises used: Equiv.Perm.mem_ofSign
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
hσ : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ : ℤˣ) (1 : ℤˣ)
hτ : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ : ℤˣ) (-1 : ℤˣ)
⊢ Eq (α := ℤˣ) 1 (-1)

Tactic:
have := hσ.symm.trans hτ
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
hσ : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ : ℤˣ) (1 : ℤˣ)
hτ : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ : ℤˣ) (-1 : ℤˣ)
this : Eq (α := ℤˣ) 1 (-1)
⊢ False

Tactic:
contradiction
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
h :
  ∀ (σ : Perm α),
    Membership.mem (γ := Finset (Perm α)) (disjUnion (ofSign 1) (ofSign (-1)) ⋯) σ ↔
      Membership.mem (γ := Finset (Perm α)) univ σ
⊢ Eq.{u + 1} (α := Finset (Perm α)) (disjUnion (ofSign 1) (ofSign (-1)) ⋯) univ

Tactic:
ext σ
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
h :
  Membership.mem (γ := Finset (Perm α)) (ofSign 1) σ ∨ Membership.mem (γ := Finset (Perm α)) (ofSign (-1)) σ ↔
    Membership.mem (γ := Finset (Perm α)) univ σ
h₁ :
  Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ : ℤˣ) (1 : ℤˣ) ∨
      Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ : ℤˣ) (-1 : ℤˣ) ↔
    Membership.mem (γ := Finset (Perm α)) univ σ
h₂ : True ↔ Membership.mem (γ := Finset (Perm α)) univ σ
⊢ Membership.mem (γ := Finset (Perm α)) (disjUnion (ofSign 1) (ofSign (-1)) ⋯) σ ↔
    Membership.mem (γ := Finset (Perm α)) univ σ

Tactic:
simp_rw [mem_disjUnion, mem_ofSign, Int.units_eq_one_or, mem_univ]

Premises used: Finset.mem_univ, Equiv.Perm.mem_ofSign, Int.units_eq_one_or, Finset.mem_disjUnion
-- Module: Mathlib.GroupTheory.Perm.Subgroup
Goal:
α : Type u_1
β : Type u_2
inst : Fintype ↥(sumCongrHom α β).range
inst_1 : Fintype (Prod.{u_1, u_2} (Perm α) (Perm β))
⊢ Fintype.card ↥(sumCongrHom α β).range = Fintype.card (Prod.{u_1, u_2} (Perm α) (Perm β))

Tactic:
Fintype.card_eq.mpr ⟨(ofInjective (sumCongrHom α β) sumCongrHom_injective).symm⟩

Premises used: Iff.mpr, Equiv.Perm.sumCongrHom, Fintype.card_eq, Nonempty.intro, Equiv.ofInjective, Equiv.Perm.sumCongrHom_injective, Equiv.symm, DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.Subgroup
Goal:
α : Type u_1
β : α → Type u_2
inst : Fintype ↥(sigmaCongrRightHom β).range
inst_1 : Fintype ((a : α) → Perm (β a))
⊢ Fintype.card ↥(sigmaCongrRightHom β).range = Fintype.card ((a : α) → Perm (β a))

Tactic:
Fintype.card_eq.mpr ⟨(ofInjective (sigmaCongrRightHom β) sigmaCongrRightHom_injective).symm⟩

Premises used: Iff.mpr, Equiv.Perm.sigmaCongrRightHom, Fintype.card_eq, Nonempty.intro, Equiv.Perm.sigmaCongrRightHom_injective, Equiv.ofInjective, Equiv.symm, DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.Subgroup
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
inst_1 : Fintype ↥(subtypeCongrHom p).range
inst_2 : Fintype (Perm { a : α // p a } × Perm { a : α // ¬p a })
⊢ Fintype.card.{u_1} ↥(subtypeCongrHom p).range = Fintype.card.{u_1} (Perm { a : α // p a } × Perm { a : α // ¬p a })

Tactic:
Fintype.card_eq.mpr ⟨(ofInjective (subtypeCongrHom p) (subtypeCongrHom_injective p)).symm⟩

Premises used: Iff.mpr, Equiv.Perm.subtypeCongrHom_injective, Fintype.card_eq, Nonempty.intro, Equiv.ofInjective, Equiv.Perm.subtypeCongrHom, Equiv.symm, DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
f g : Perm α
⊢ f.Disjoint g → g.Disjoint f

Tactic:
simp only [Disjoint, or_comm, imp_self]

Premises used: imp_self, or_comm, Equiv.Perm.Disjoint
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
⊢ Symmetric.{u_1 + 1} (α := Perm α) Disjoint

Tactic:
fun _ _ => Disjoint.symm

Premises used: Equiv.Perm.Disjoint.symm, Symmetric
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
f g h : Perm α
⊢ Std.Symm.{max 1 (u_1 + 1)} (α := Perm α) Disjoint

Tactic:
⟨Disjoint.symmetric⟩

Premises used: Std.Symm.mk, Equiv.Perm.Disjoint.symmetric
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
f g : Perm α
⊢ f.Disjoint g ↔ g.Disjoint f

Tactic:
⟨Disjoint.symm, Disjoint.symm⟩

Premises used: Equiv.Perm.Disjoint.symm, Iff.intro
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
f g : Perm α
h : f.Disjoint g
x : α
hf : (f : (a : α) → α) x = x
hg : Eq (α := α) ((f : (a : α) → α) ((g : (a : α) → α) x : α) : α) ((g : (a : α) → α) x : α)
⊢ Eq (α := α) ((f * g : (a : α) → α) x : α) ((g * f : (a : α) → α) x : α)

Tactic:
simp [mul_apply, hf, hg]

Premises used: Equiv.Perm.mul_apply
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
f g : Perm α
h : f.Disjoint g
x : α
hf : (f : (a : α) → α) x = x
hg : Eq (α := α) ((g : (a : α) → α) ((g : (a : α) → α) x : α) : α) ((g : (a : α) → α) x : α)
⊢ Eq (α := α) ((f * g : (a : α) → α) x : α) ((g * f : (a : α) → α) x : α)

Tactic:
simp [mul_apply, hf, g.injective hg]

Premises used: Equiv.Perm.mul_apply, Equiv.injective
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
f g : Perm α
h : f.Disjoint g
x : α
hg : (g : (a : α) → α) x = x
hf : Eq (α := α) ((f : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α)
⊢ Eq (α := α) ((f * g : (a : α) → α) x : α) ((g * f : (a : α) → α) x : α)

Tactic:
simp [mul_apply, f.injective hf, hg]

Premises used: Equiv.Perm.mul_apply, Equiv.injective
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
f g : Perm α
h : f.Disjoint g
x : α
hg : (g : (a : α) → α) x = x
hf : Eq (α := α) ((g : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α)
⊢ Eq (α := α) ((f * g : (a : α) → α) x : α) ((g * f : (a : α) → α) x : α)

Tactic:
simp [mul_apply, hf, hg]

Premises used: Equiv.Perm.mul_apply
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
f : Perm α
⊢ Disjoint 1 f

Tactic:
fun _ => Or.inl rfl

Premises used: Or.inl, rfl, Equiv.Perm.Disjoint
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
f : Perm α
⊢ f.Disjoint 1

Tactic:
fun _ => Or.inr rfl

Premises used: Or.inr, rfl, Equiv.Perm.Disjoint
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
f g : Perm α
⊢ f.Disjoint g ↔ ∀ (x : α), (f : (a : α) → α) x = x ∨ (g : (a : α) → α) x = x

Tactic:
Iff.rfl

Premises used: Iff.rfl, Equiv.Perm.Disjoint
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
f : Perm α
⊢ f.Disjoint f ↔ f = 1

Tactic:
⟨fun h => ?_, fun h => h.symm ▸ disjoint_one_left 1⟩

Premises used: Equiv.Perm.disjoint_one_left, Eq.rec, Iff.intro, OfNat.ofNat, Eq.symm
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
f : Perm α
refine : ∀ (h : f.Disjoint f), f = 1
⊢ f.Disjoint f ↔ f = 1

Tactic:
refine ⟨fun h => ?_, fun h => h.symm ▸ disjoint_one_left 1⟩
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
f : Perm α
h : f.Disjoint f
H : ∀ (x : α), Eq (α := α) ((f : (a : α) → α) x : α) ((1 : (a : α) → α) x : α)
⊢ f = 1

Tactic:
ext x
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
f : Perm α
h : f.Disjoint f
x : α
H H₁ : ∀ (hx : (f : (a : α) → α) x = x), Eq (α := α) ((f : (a : α) → α) x : α) ((1 : (a : α) → α) x : α)
⊢ Eq (α := α) ((f : (a : α) → α) x : α) ((1 : (a : α) → α) x : α)

Tactic:
rcases h x with hx | hx
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
f : Perm α
h : f.Disjoint f
x : α
hx : (f : (a : α) → α) x = x
⊢ Eq (α := α) ((f : (a : α) → α) x : α) ((1 : (a : α) → α) x : α)

Tactic:
simp [hx]
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
f g : Perm α
h : f.Disjoint g
x : α
rw : (f : (a : α) → α) x = x ∨ (g : (a : α) → α) x = x
⊢ (f⁻¹ : (a : α) → α) x = x ∨ (g : (a : α) → α) x = x

Tactic:
rw [inv_eq_iff_eq, eq_comm]

Premises used: Equiv.Perm.inv_eq_iff_eq, eq_comm
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
f g : Perm α
h : f.Disjoint g
x : α
⊢ (f : (a : α) → α) x = x ∨ (g : (a : α) → α) x = x

Tactic:
h x
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
f g : Perm α
h : f.Disjoint g
x : α
⊢ (f : (a : α) → α) x = x ∨ (g : (a : α) → α) x = x

Tactic:
exact h x
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
f g : Perm α
h : f.Disjoint g
⊢ f.Disjoint g⁻¹

Tactic:
h.symm.inv_left.symm

Premises used: Equiv.Perm.Disjoint.symm, Equiv.Perm.Disjoint.inv_left
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
f g : Perm α
⊢ f⁻¹.Disjoint g ↔ f.Disjoint g

Tactic:
⟨fun h => ?_, Disjoint.inv_left⟩

Premises used: Equiv.Perm.Disjoint.inv_left, Iff.intro
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
f g : Perm α
refine : ∀ (h : f⁻¹.Disjoint g), f.Disjoint g
⊢ f⁻¹.Disjoint g ↔ f.Disjoint g

Tactic:
refine ⟨fun h => ?_, Disjoint.inv_left⟩
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
f g : Perm α
h : f⁻¹.Disjoint g
⊢ f⁻¹⁻¹.Disjoint g

Tactic:
h.inv_left

Premises used: Equiv.Perm.Disjoint.inv_left
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
f g : Perm α
h : f⁻¹.Disjoint g
⊢ f.Disjoint g

Tactic:
convert! h.inv_left

Premises used: Equiv.Perm.Disjoint.inv_left
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
f g : Perm α
rw : g⁻¹.Disjoint f ↔ f.Disjoint g
rw₁ : g.Disjoint f ↔ f.Disjoint g
rw₂ rw₃ : f.Disjoint g ↔ f.Disjoint g
⊢ f.Disjoint g⁻¹ ↔ f.Disjoint g

Tactic:
rw [disjoint_comm, disjoint_inv_left_iff, disjoint_comm]

Premises used: Equiv.Perm.disjoint_comm, Equiv.Perm.disjoint_inv_left_iff
-- Module: Mathlib.GroupTheory.Perm.Support
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
inr : (h : (a : α) → α) x = x → (f * g : (a : α) → α) x = x ∨ (h : (a : α) → α) x = x
⊢ (f * g : (a : α) → α) x = x ∨ (h : (a : α) → α) x = x

Tactic:
cases H1 x
-- Module: Mathlib.GroupTheory.Perm.Support
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
inl₁ : (h : (a : α) → α) x = x → (f * g : (a : α) → α) x = x ∨ (h : (a : α) → α) x = x
⊢ (f * g : (a : α) → α) x = x ∨ (h : (a : α) → α) x = x

Tactic:
cases H2 x
-- Module: Mathlib.GroupTheory.Perm.Support
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
inr₁ : (h : (a : α) → α) x = x → (f * g : (a : α) → α) x = x ∨ (h : (a : α) → α) x = x
⊢ (f * g : (a : α) → α) x = x ∨ (h : (a : α) → α) x = x

Tactic:
cases H2 x
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
f g h : Perm α
H1 : f.Disjoint h
H2 : g.Disjoint h
x : α
h_1 : (f : (a : α) → α) x = x
h_2 : (g : (a : α) → α) x = x
⊢ (f * g : (a : α) → α) x = x ∨ (h : (a : α) → α) x = x

Tactic:
simp [*]
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
f g h : Perm α
H1 : f.Disjoint h
H2 : g.Disjoint h
x : α
h_1 : (f : (a : α) → α) x = x
h_2 : (h : (a : α) → α) x = x
⊢ (f * g : (a : α) → α) x = x ∨ (h : (a : α) → α) x = x

Tactic:
simp [*]
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
f g h : Perm α
H1 : f.Disjoint h
H2 : g.Disjoint h
x : α
h_1 : (h : (a : α) → α) x = x
h_2 : (g : (a : α) → α) x = x
⊢ (f * g : (a : α) → α) x = x ∨ (h : (a : α) → α) x = x

Tactic:
simp [*]
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
f g h : Perm α
H1 : f.Disjoint h
H2 : g.Disjoint h
x : α
h_1 h_2 : (h : (a : α) → α) x = x
⊢ (f * g : (a : α) → α) x = x ∨ (h : (a : α) → α) x = x

Tactic:
simp [*]
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
f g h : Perm α
H1 : f.Disjoint g
H2 : f.Disjoint h
rw : (g * h).Disjoint f
⊢ f.Disjoint (g * h)

Tactic:
rw [disjoint_comm]

Premises used: Equiv.Perm.disjoint_comm
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
f g h : Perm α
H1 : f.Disjoint g
H2 : f.Disjoint h
⊢ (g * h).Disjoint f

Tactic:
H1.symm.mul_left H2.symm

Premises used: Equiv.Perm.Disjoint.symm, Equiv.Perm.Disjoint.mul_left
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
f g h : Perm α
H1 : f.Disjoint g
H2 : f.Disjoint h
⊢ (g * h).Disjoint f

Tactic:
exact H1.symm.mul_left H2.symm

Premises used: Equiv.Perm.Disjoint.symm, Equiv.Perm.Disjoint.mul_left
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
f g h : Perm α
x : α
⊢ (h * f * h⁻¹ : (a : α) → α) x = x ∨ (h * g * h⁻¹ : (a : α) → α) x = x ↔
    Eq (α := α) ((f : (a : α) → α) ((h⁻¹ : (a : α) → α) x : α) : α) ((h⁻¹ : (a : α) → α) x : α) ∨
      Eq (α := α) ((g : (a : α) → α) ((h⁻¹ : (a : α) → α) x : α) : α) ((h⁻¹ : (a : α) → α) x : α)

Tactic:
simp only [mul_apply, eq_inv_iff_eq]

Premises used: Equiv.Perm.mul_apply, Equiv.Perm.eq_inv_iff_eq
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
f g : Perm α
H : f.Disjoint g
h : Perm α
⊢ (h * f * h⁻¹).Disjoint (h * g * h⁻¹)

Tactic:
(disjoint_conj h).2 H

Premises used: Iff.mpr, Equiv.Perm.disjoint_conj