awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
inst : Finite α
σ τ π ρ : Perm α
hc1 : IsConj σ π
hc2 : IsConj τ ρ
hd1 : σ.Disjoint τ
hd2 : π.Disjoint ρ
⊢ IsConj (σ * τ) (π * ρ)
have intro : ∀ (val : Fintype α), IsConj (σ * τ) (π * ρ)
Tactic: classical
  cases nonempty_fintype α
  obtain ⟨f, rfl⟩ := isConj_iff.1 hc1
  obtain ⟨g, rfl⟩ := isConj_iff.1 hc2
  have hd1' := coe_inj.2 hd1.support_mul
  have hd2' := coe_inj.2 hd2.support_mul
  rw [coe_union] at *
  have hd1'' := disjoint_coe.2 (disjoint_iff_disjoint_support.1 hd1)
  have hd2'' := disjoint_coe.2 (disjoint_iff_disjoint_support.1 hd2)
  refine isConj_of_support_equiv ?_ ?_
  · refine ((Equiv.setCongr hd1').trans (Equiv.Set.union hd1'')).trans <|
      (Equiv.sumCongr (subtypeEquiv f fun a => ?_) <| subtypeEquiv g fun a => ?_).trans
        ((Equiv.setCongr hd2').trans (Equiv.Set.union hd2'')).symm <;>
      simp only [Set.mem_image, toEmbedding_apply, exists_eq_right, support_conj, coe_map,
        apply_eq_iff_eq]
  intro x hx
  simp only [trans_apply, symm_trans_apply, Equiv.setCongr_apply, Equiv.setCongr_symm_apply,
    Equiv.sumCongr_apply]
  rw [hd1', Set.mem_union] at hx
  rcases hx with hxσ | hxτ
  · rw [mem_coe, mem_support] at hxσ
    rw [Set.union_apply_left, Set.union_apply_left]
    · simp only [subtypeEquiv_apply, Perm.coe_mul, Sum.map_inl, comp_apply,
        Set.union_symm_apply_left, Subtype.coe_mk, apply_eq_iff_eq, coe_inv]
      have h := (hd2 (f x)).resolve_left ?_
      · rw [mul_apply, mul_apply, coe_inv] at h
        rw [h, symm_apply_apply, (hd1 x).resolve_left hxσ]
      · rwa [mul_apply, mul_apply, coe_inv, symm_apply_apply, apply_eq_iff_eq]
    · rwa [Subtype.coe_mk, mem_coe, mem_support]
    · rwa [Subtype.coe_mk, Perm.mul_apply, (hd1 x).resolve_left hxσ, mem_coe,
        apply_mem_support, mem_support]
  · rw [mem_coe, ← apply_mem_support, mem_support] at hxτ
    rw [Set.union_apply_right, Set.union_apply_right]
    · simp only [subtypeEquiv_apply, Perm.coe_mul, Sum.map_inr, comp_apply,
        Set.union_symm_apply_right, Subtype.coe_mk]
      have h := (hd2 (g (τ x))).resolve_right ?_
      · rw [mul_apply, mul_apply, coe_inv] at h
        rw [coe_inv, coe_inv, symm_apply_apply, h, (hd1 (τ x)).resolve_right hxτ]
      · rwa [mul_apply, mul_apply, coe_inv, symm_apply_apply, apply_eq_iff_eq]
    · rwa [Subtype.coe_mk, mem_coe, ← apply_mem_support, mem_support]
    · rwa [Subtype.coe_mk, Perm.mul_apply, (hd1 (τ x)).resolve_right hxτ,
        mem_coe, mem_support]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
inst : Finite α
σ τ π ρ : Perm α
hc1 : IsConj σ π
hc2 : IsConj τ ρ
hd1 : σ.Disjoint τ
hd2 : π.Disjoint ρ
intro : ∀ (val : Fintype α), IsConj (σ * τ) (π * ρ)
⊢ IsConj (σ * τ) (π * ρ)
have intro₁ : ∀ (val : Fintype α) (f : Perm α) (hc1 : IsConj σ (f * σ * f⁻¹)) (hd2 : (f * σ * f⁻¹).Disjoint ρ),
  IsConj (σ * τ) (f * σ * f⁻¹ * ρ)
Tactic: classical
  cases nonempty_fintype α
  obtain ⟨f, rfl⟩ := isConj_iff.1 hc1
  obtain ⟨g, rfl⟩ := isConj_iff.1 hc2
  have hd1' := coe_inj.2 hd1.support_mul
  have hd2' := coe_inj.2 hd2.support_mul
  rw [coe_union] at *
  have hd1'' := disjoint_coe.2 (disjoint_iff_disjoint_support.1 hd1)
  have hd2'' := disjoint_coe.2 (disjoint_iff_disjoint_support.1 hd2)
  refine isConj_of_support_equiv ?_ ?_
  · refine ((Equiv.setCongr hd1').trans (Equiv.Set.union hd1'')).trans <|
      (Equiv.sumCongr (subtypeEquiv f fun a => ?_) <| subtypeEquiv g fun a => ?_).trans
        ((Equiv.setCongr hd2').trans (Equiv.Set.union hd2'')).symm <;>
      simp only [Set.mem_image, toEmbedding_apply, exists_eq_right, support_conj, coe_map,
        apply_eq_iff_eq]
  intro x hx
  simp only [trans_apply, symm_trans_apply, Equiv.setCongr_apply, Equiv.setCongr_symm_apply,
    Equiv.sumCongr_apply]
  rw [hd1', Set.mem_union] at hx
  rcases hx with hxσ | hxτ
  · rw [mem_coe, mem_support] at hxσ
    rw [Set.union_apply_left, Set.union_apply_left]
    · simp only [subtypeEquiv_apply, Perm.coe_mul, Sum.map_inl, comp_apply,
        Set.union_symm_apply_left, Subtype.coe_mk, apply_eq_iff_eq, coe_inv]
      have h := (hd2 (f x)).resolve_left ?_
      · rw [mul_apply, mul_apply, coe_inv] at h
        rw [h, symm_apply_apply, (hd1 x).resolve_left hxσ]
      · rwa [mul_apply, mul_apply, coe_inv, symm_apply_apply, apply_eq_iff_eq]
    · rwa [Subtype.coe_mk, mem_coe, mem_support]
    · rwa [Subtype.coe_mk, Perm.mul_apply, (hd1 x).resolve_left hxσ, mem_coe,
        apply_mem_support, mem_support]
  · rw [mem_coe, ← apply_mem_support, mem_support] at hxτ
    rw [Set.union_apply_right, Set.union_apply_right]
    · simp only [subtypeEquiv_apply, Perm.coe_mul, Sum.map_inr, comp_apply,
        Set.union_symm_apply_right, Subtype.coe_mk]
      have h := (hd2 (g (τ x))).resolve_right ?_
      · rw [mul_apply, mul_apply, coe_inv] at h
        rw [coe_inv, coe_inv, symm_apply_apply, h, (hd1 (τ x)).resolve_right hxτ]
      · rwa [mul_apply, mul_apply, coe_inv, symm_apply_apply, apply_eq_iff_eq]
    · rwa [Subtype.coe_mk, mem_coe, ← apply_mem_support, mem_support]
    · rwa [Subtype.coe_mk, Perm.mul_apply, (hd1 (τ x)).resolve_right hxτ,
        mem_coe, mem_support]
Cleared hypotheses: π, hc1, hd2
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
inst : Finite α
σ τ π ρ : Perm α
hc1 : IsConj σ π
hc2 : IsConj τ ρ
hd1 : σ.Disjoint τ
hd2 : π.Disjoint ρ
intro : ∀ (val : Fintype α), IsConj (σ * τ) (π * ρ)
intro₁ :
  ∀ (val : Fintype α) (f : Perm α) (hc1 : IsConj σ (f * σ * f⁻¹)) (hd2 : (f * σ * f⁻¹).Disjoint ρ),
    IsConj (σ * τ) (f * σ * f⁻¹ * ρ)
⊢ IsConj (σ * τ) (π * ρ)
have intro₂ : ∀ (val : Fintype α) (f : Perm α) (hc1 : IsConj σ (f * σ * f⁻¹)) (g : Perm α) (hc2 : IsConj τ (g * τ * g⁻¹))
  (hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)), IsConj (σ * τ) (f * σ * f⁻¹ * (g * τ * g⁻¹))
Tactic: classical
  cases nonempty_fintype α
  obtain ⟨f, rfl⟩ := isConj_iff.1 hc1
  obtain ⟨g, rfl⟩ := isConj_iff.1 hc2
  have hd1' := coe_inj.2 hd1.support_mul
  have hd2' := coe_inj.2 hd2.support_mul
  rw [coe_union] at *
  have hd1'' := disjoint_coe.2 (disjoint_iff_disjoint_support.1 hd1)
  have hd2'' := disjoint_coe.2 (disjoint_iff_disjoint_support.1 hd2)
  refine isConj_of_support_equiv ?_ ?_
  · refine ((Equiv.setCongr hd1').trans (Equiv.Set.union hd1'')).trans <|
      (Equiv.sumCongr (subtypeEquiv f fun a => ?_) <| subtypeEquiv g fun a => ?_).trans
        ((Equiv.setCongr hd2').trans (Equiv.Set.union hd2'')).symm <;>
      simp only [Set.mem_image, toEmbedding_apply, exists_eq_right, support_conj, coe_map,
        apply_eq_iff_eq]
  intro x hx
  simp only [trans_apply, symm_trans_apply, Equiv.setCongr_apply, Equiv.setCongr_symm_apply,
    Equiv.sumCongr_apply]
  rw [hd1', Set.mem_union] at hx
  rcases hx with hxσ | hxτ
  · rw [mem_coe, mem_support] at hxσ
    rw [Set.union_apply_left, Set.union_apply_left]
    · simp only [subtypeEquiv_apply, Perm.coe_mul, Sum.map_inl, comp_apply,
        Set.union_symm_apply_left, Subtype.coe_mk, apply_eq_iff_eq, coe_inv]
      have h := (hd2 (f x)).resolve_left ?_
      · rw [mul_apply, mul_apply, coe_inv] at h
        rw [h, symm_apply_apply, (hd1 x).resolve_left hxσ]
      · rwa [mul_apply, mul_apply, coe_inv, symm_apply_apply, apply_eq_iff_eq]
    · rwa [Subtype.coe_mk, mem_coe, mem_support]
    · rwa [Subtype.coe_mk, Perm.mul_apply, (hd1 x).resolve_left hxσ, mem_coe,
        apply_mem_support, mem_support]
  · rw [mem_coe, ← apply_mem_support, mem_support] at hxτ
    rw [Set.union_apply_right, Set.union_apply_right]
    · simp only [subtypeEquiv_apply, Perm.coe_mul, Sum.map_inr, comp_apply,
        Set.union_symm_apply_right, Subtype.coe_mk]
      have h := (hd2 (g (τ x))).resolve_right ?_
      · rw [mul_apply, mul_apply, coe_inv] at h
        rw [coe_inv, coe_inv, symm_apply_apply, h, (hd1 (τ x)).resolve_right hxτ]
      · rwa [mul_apply, mul_apply, coe_inv, symm_apply_apply, apply_eq_iff_eq]
    · rwa [Subtype.coe_mk, mem_coe, ← apply_mem_support, mem_support]
    · rwa [Subtype.coe_mk, Perm.mul_apply, (hd1 (τ x)).resolve_right hxτ,
        mem_coe, mem_support]
Cleared hypotheses: π, ρ, hc1, hc2, hd2
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (hypothesis)
Goal:
α : Type u
g p : Perm α
hp : Membership.mem (γ := Subgroup (Perm α)) (Subgroup.centralizer {g}) p
x : α
⊢ Membership.mem (α := α) (γ := Set α) (fixedPoints (⇑g : (a : α) → α)) ((p : (a : α) → α) x : α) ↔
    Membership.mem (γ := Set α) (fixedPoints (⇑g : (a : α) → α)) x
have hp₁ : p * g = g * p
Tactic: simp only [Subgroup.mem_centralizer_singleton_iff] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
g p : Perm α
x : α
hp : p * g = g * p
⊢ Eq (α := α) ((g : (a : α) → α) ((p : (a : α) → α) x : α) : α) ((p : (a : α) → α) x : α) ↔ (g : (a : α) → α) x = x
have rw : Eq (α := α) ((g * p : (a : α) → α) x : α) ((p : (a : α) → α) x : α) ↔ (g : (a : α) → α) x = x
Tactic: rw [← mul_apply, ← hp, mul_apply, EmbeddingLike.apply_eq_iff_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
g p : Perm α
x : α
hp : p * g = g * p
rw : Eq (α := α) ((g * p : (a : α) → α) x : α) ((p : (a : α) → α) x : α) ↔ (g : (a : α) → α) x = x
⊢ Eq (α := α) ((g : (a : α) → α) ((p : (a : α) → α) x : α) : α) ((p : (a : α) → α) x : α) ↔ (g : (a : α) → α) x = x
have rw₁ : Eq (α := α) ((p * g : (a : α) → α) x : α) ((p : (a : α) → α) x : α) ↔ (g : (a : α) → α) x = x
Tactic: rw [← mul_apply, ← hp, mul_apply, EmbeddingLike.apply_eq_iff_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
g p : Perm α
x : α
hp : p * g = g * p
rw : Eq (α := α) ((g * p : (a : α) → α) x : α) ((p : (a : α) → α) x : α) ↔ (g : (a : α) → α) x = x
rw₁ : Eq (α := α) ((p * g : (a : α) → α) x : α) ((p : (a : α) → α) x : α) ↔ (g : (a : α) → α) x = x
⊢ Eq (α := α) ((g : (a : α) → α) ((p : (a : α) → α) x : α) : α) ((p : (a : α) → α) x : α) ↔ (g : (a : α) → α) x = x
have rw₂ : Eq (α := α) ((p : (a : α) → α) ((g : (a : α) → α) x : α) : α) ((p : (a : α) → α) x : α) ↔ (g : (a : α) → α) x = x
Tactic: rw [← mul_apply, ← hp, mul_apply, EmbeddingLike.apply_eq_iff_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
g p : Perm α
x : α
hp : p * g = g * p
rw : Eq (α := α) ((g * p : (a : α) → α) x : α) ((p : (a : α) → α) x : α) ↔ (g : (a : α) → α) x = x
rw₁ : Eq (α := α) ((p * g : (a : α) → α) x : α) ((p : (a : α) → α) x : α) ↔ (g : (a : α) → α) x = x
rw₂ : Eq (α := α) ((p : (a : α) → α) ((g : (a : α) → α) x : α) : α) ((p : (a : α) → α) x : α) ↔ (g : (a : α) → α) x = x
⊢ Eq (α := α) ((g : (a : α) → α) ((p : (a : α) → α) x : α) : α) ((p : (a : α) → α) x : α) ↔ (g : (a : α) → α) x = x
have rw₃ : (g : (a : α) → α) x = x ↔ (g : (a : α) → α) x = x
Tactic: rw [← mul_apply, ← hp, mul_apply, EmbeddingLike.apply_eq_iff_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
inst : DecidableEq α
g : Perm α
u : Perm (↑(fixedPoints (⇑g : (a : α) → α)) : Type u)
x : α
⊢ (((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (fixedPoints (⇑g : (a : α) → α)) x) :
                (a : Perm { x : α // x ∈ fixedPoints (⇑g : (a : α) → α) }) → Perm α)
              u :
            Perm α) :
          (a : α) → α)
        x =
      x ∨
    (g : (a : α) → α) x = x
have pos : ∀ (hx : Membership.mem (γ := Set α) (fixedPoints (⇑g : (a : α) → α)) x),
  (((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (fixedPoints (⇑g : (a : α) → α)) x) :
                (a : Perm { x : α // x ∈ fixedPoints (⇑g : (a : α) → α) }) → Perm α)
              u :
            Perm α) :
          (a : α) → α)
        x =
      x ∨
    (g : (a : α) → α) x = x
Tactic: by_cases hx : x ∈ Function.fixedPoints g
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
inst : DecidableEq α
g : Perm α
u : Perm (↑(fixedPoints (⇑g : (a : α) → α)) : Type u)
x : α
pos :
  ∀ (hx : Membership.mem (γ := Set α) (fixedPoints (⇑g : (a : α) → α)) x),
    (((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (fixedPoints (⇑g : (a : α) → α)) x) :
                  (a : Perm { x : α // x ∈ fixedPoints (⇑g : (a : α) → α) }) → Perm α)
                u :
              Perm α) :
            (a : α) → α)
          x =
        x ∨
      (g : (a : α) → α) x = x
⊢ (((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (fixedPoints (⇑g : (a : α) → α)) x) :
                (a : Perm { x : α // x ∈ fixedPoints (⇑g : (a : α) → α) }) → Perm α)
              u :
            Perm α) :
          (a : α) → α)
        x =
      x ∨
    (g : (a : α) → α) x = x
have neg : ∀ (hx : x ∉ fixedPoints (⇑g : (a : α) → α)),
  (((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (fixedPoints (⇑g : (a : α) → α)) x) :
                (a : Perm { x : α // x ∈ fixedPoints (⇑g : (a : α) → α) }) → Perm α)
              u :
            Perm α) :
          (a : α) → α)
        x =
      x ∨
    (g : (a : α) → α) x = x
Tactic: by_cases hx : x ∈ Function.fixedPoints g
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
inst : DecidableEq α
g : Perm α
u : Perm (↑(fixedPoints (⇑g : (a : α) → α)) : Type u)
x : α
hx : Membership.mem (γ := Set α) (fixedPoints (⇑g : (a : α) → α)) x
⊢ (((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (fixedPoints (⇑g : (a : α) → α)) x) :
                (a : Perm { x : α // x ∈ fixedPoints (⇑g : (a : α) → α) }) → Perm α)
              u :
            Perm α) :
          (a : α) → α)
        x =
      x ∨
    (g : (a : α) → α) x = x
have pos : (g : (a : α) → α) x = x
Tactic: right
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
inst : DecidableEq α
g : Perm α
u : Perm (↑(fixedPoints (⇑g : (a : α) → α)) : Type u)
x : α
hx : x ∉ fixedPoints (⇑g : (a : α) → α)
⊢ (((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (fixedPoints (⇑g : (a : α) → α)) x) :
                (a : Perm { x : α // x ∈ fixedPoints (⇑g : (a : α) → α) }) → Perm α)
              u :
            Perm α) :
          (a : α) → α)
        x =
      x ∨
    (g : (a : α) → α) x = x
have neg : (((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (fixedPoints (⇑g : (a : α) → α)) x) :
            (a : Perm { x : α // x ∈ fixedPoints (⇑g : (a : α) → α) }) → Perm α)
          u :
        Perm α) :
      (a : α) → α)
    x =
  x
Tactic: left
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
inst : DecidableEq α
g : Perm α
u : Perm (↑(fixedPoints (⇑g : (a : α) → α)) : Type u)
x : α
hx : x ∉ fixedPoints (⇑g : (a : α) → α)
⊢ (((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (fixedPoints (⇑g : (a : α) → α)) x) :
              (a : Perm { x : α // x ∈ fixedPoints (⇑g : (a : α) → α) }) → Perm α)
            u :
          Perm α) :
        (a : α) → α)
      x =
    x
have neg : x = x
Tactic: rw [ofSubtype_apply_of_not_mem u hx]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
n : ℕ
h : n.Coprime (orderOf σ)
⊢ (σ ^ n).support = σ.support
have obtain : ∀ (m : ℕ) (hm : (σ ^ n) ^ m = σ), (σ ^ n).support = σ.support
Tactic: obtain ⟨m, hm⟩ := exists_pow_eq_self_of_coprime h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
x : Perm (↑(fixedPoints (⇑σ : (a : α) → α)) : Type u)
⊢ _root_.Disjoint
    (support
      ((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (fixedPoints (⇑σ : (a : α) → α)) x) :
          (a : Perm { x : α // x ∈ fixedPoints (⇑σ : (a : α) → α) }) → Perm α)
        x))
    σ.support
have rw : ∀ (a : α),
  Membership.mem (γ := Finset α)
      (support
        ((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (fixedPoints (⇑σ : (a : α) → α)) x) :
            (a : Perm { x : α // x ∈ fixedPoints (⇑σ : (a : α) → α) }) → Perm α)
          x))
      a →
    ∀ b ∈ σ.support, a ≠ b
Tactic: rw [Finset.disjoint_iff_ne]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (hypothesis)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
x : Perm (↑(fixedPoints (⇑σ : (a : α) → α)) : Type u)
a : α
ha :
  Membership.mem (γ := Finset α)
    (support
      ((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (fixedPoints (⇑σ : (a : α) → α)) x) :
          (a : Perm { x : α // x ∈ fixedPoints (⇑σ : (a : α) → α) }) → Perm α)
        x))
    a
hb : a ∈ σ.support
⊢ False
have ha₁ : (((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (fixedPoints (⇑σ : (a : α) → α)) x) :
            (a : Perm { x : α // x ∈ fixedPoints (⇑σ : (a : α) → α) }) → Perm α)
          x :
        Perm α) :
      (a : α) → α)
    a ≠
  a
Tactic: rw [mem_support] at ha hb
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (hypothesis)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
x : Perm (↑(fixedPoints (⇑σ : (a : α) → α)) : Type u)
a : α
ha :
  Membership.mem (γ := Finset α)
    (support
      ((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (fixedPoints (⇑σ : (a : α) → α)) x) :
          (a : Perm { x : α // x ∈ fixedPoints (⇑σ : (a : α) → α) }) → Perm α)
        x))
    a
hb : a ∈ σ.support
ha₁ :
  (((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (fixedPoints (⇑σ : (a : α) → α)) x) :
              (a : Perm { x : α // x ∈ fixedPoints (⇑σ : (a : α) → α) }) → Perm α)
            x :
          Perm α) :
        (a : α) → α)
      a ≠
    a
⊢ False
have hb₁ : (σ : (a : α) → α) a ≠ a
Tactic: rw [mem_support] at ha hb
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
H K : Subgroup (Perm α)
h : ∀ a ∈ H, ∀ b ∈ K, _root_.Disjoint a.support b.support
⊢ _root_.Disjoint H K
have rw : H ⊓ K ≤ ⊥
Tactic: rw [disjoint_iff_inf_le]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
H K : Subgroup (Perm α)
h : ∀ a ∈ H, ∀ b ∈ K, _root_.Disjoint a.support b.support
x : Perm α
⊢ x ∈ H ⊓ K → Membership.mem (γ := Subgroup (Perm α)) ⊥ x
have this : ∀ (hx1 : x ∈ (↑H.toSubmonoid : Set (Perm α))) (hx2 : x ∈ (↑K.toSubmonoid : Set (Perm α))),
  Membership.mem (γ := Subgroup (Perm α)) ⊥ x
Tactic: ⟨hx1, hx2⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (hypothesis)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
H K : Subgroup (Perm α)
h : ∀ a ∈ H, ∀ b ∈ K, _root_.Disjoint a.support b.support
x : Perm α
hx1 : x ∈ (↑H.toSubmonoid : Set (Perm α))
hx2 : x ∈ (↑K.toSubmonoid : Set (Perm α))
⊢ Membership.mem (γ := Subgroup (Perm α)) ⊥ x
have h₁ : _root_.Disjoint x.support x.support
Tactic: specialize h x hx1 x hx2
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
H K : Subgroup (Perm α)
x : Perm α
hx1 : x ∈ (↑H.toSubmonoid : Set (Perm α))
hx2 : x ∈ (↑K.toSubmonoid : Set (Perm α))
h : _root_.Disjoint x.support x.support
⊢ Membership.mem (γ := Subgroup (Perm α)) ⊥ x
have rwa : ∀ (h : x.support = ⊥), Membership.mem (γ := Subgroup (Perm α)) ⊥ x
Tactic: rwa [disjoint_self, Finset.bot_eq_empty, support_eq_empty_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
H K : Subgroup (Perm α)
x : Perm α
hx1 : x ∈ (↑H.toSubmonoid : Set (Perm α))
hx2 : x ∈ (↑K.toSubmonoid : Set (Perm α))
h : _root_.Disjoint x.support x.support
rwa : ∀ (h : x.support = ⊥), Membership.mem (γ := Subgroup (Perm α)) ⊥ x
⊢ Membership.mem (γ := Subgroup (Perm α)) ⊥ x
have rwa₁ : ∀ (h : x.support = ∅), Membership.mem (γ := Subgroup (Perm α)) ⊥ x
Tactic: rwa [disjoint_self, Finset.bot_eq_empty, support_eq_empty_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
H K : Subgroup (Perm α)
x : Perm α
hx1 : x ∈ (↑H.toSubmonoid : Set (Perm α))
hx2 : x ∈ (↑K.toSubmonoid : Set (Perm α))
h : _root_.Disjoint x.support x.support
rwa : ∀ (h : x.support = ⊥), Membership.mem (γ := Subgroup (Perm α)) ⊥ x
rwa₁ : ∀ (h : x.support = ∅), Membership.mem (γ := Subgroup (Perm α)) ⊥ x
⊢ Membership.mem (γ := Subgroup (Perm α)) ⊥ x
have rwa₂ : ∀ (h : x = 1), Membership.mem (γ := Subgroup (Perm α)) ⊥ x
Tactic: rwa [disjoint_self, Finset.bot_eq_empty, support_eq_empty_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
S : Set (Perm α)
⊢ ∀ (a : Perm α),
    Membership.mem (γ := Subgroup (Perm α)) (closure S) a → (↑a.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)
have mem : ∀ (x : Perm α) (hx : x ∈ S), (↑x.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)
Tactic: apply closure_induction
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
S : Set (Perm α)
mem : ∀ (x : Perm α) (hx : x ∈ S), (↑x.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)
⊢ ∀ (a : Perm α),
    Membership.mem (γ := Subgroup (Perm α)) (closure S) a → (↑a.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)
have one : (↑(support 1) : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)
Tactic: apply closure_induction
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
S : Set (Perm α)
mem : ∀ (x : Perm α) (hx : x ∈ S), (↑x.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)
one : (↑(support 1) : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)
⊢ ∀ (a : Perm α),
    Membership.mem (γ := Subgroup (Perm α)) (closure S) a → (↑a.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)
have mul : ∀ (x y : Perm α) (hx : Membership.mem (γ := Subgroup (Perm α)) (closure S) x)
  (hy : Membership.mem (γ := Subgroup (Perm α)) (closure S) y),
  (↑x.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α) →
    (↑y.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α) → (↑(x * y).support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)
Tactic: apply closure_induction
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
S : Set (Perm α)
mem : ∀ (x : Perm α) (hx : x ∈ S), (↑x.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)
one : (↑(support 1) : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)
mul :
  ∀ (x y : Perm α) (hx : Membership.mem (γ := Subgroup (Perm α)) (closure S) x)
    (hy : Membership.mem (γ := Subgroup (Perm α)) (closure S) y),
    (↑x.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α) →
      (↑y.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α) → (↑(x * y).support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)
⊢ ∀ (a : Perm α),
    Membership.mem (γ := Subgroup (Perm α)) (closure S) a → (↑a.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)
have inv : ∀ (x : Perm α) (hx : Membership.mem (γ := Subgroup (Perm α)) (closure S) x),
  (↑x.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α) → (↑x⁻¹.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)
Tactic: apply closure_induction
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
S : Set (Perm α)
a b : Perm α
ha : Membership.mem (γ := Subgroup (Perm α)) (closure S) a
hb : Membership.mem (γ := Subgroup (Perm α)) (closure S) b
hc : (↑a.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)
hd : (↑b.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)
⊢ (↑(a * b).support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)
have mul : (↑(a.support ⊔ b.support) : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)
Tactic: refine (Finset.coe_subset.mpr (support_mul_le a b)).trans ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
S : Set (Perm α)
a b : Perm α
ha : Membership.mem (γ := Subgroup (Perm α)) (closure S) a
hb : Membership.mem (γ := Subgroup (Perm α)) (closure S) b
hc : (↑a.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)
hd : (↑b.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)
⊢ (↑(a.support ⊔ b.support) : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)
have mul : (↑a.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α) ∧ (↑b.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)
Tactic: rw [Finset.sup_eq_union, Finset.coe_union, Set.union_subset_iff]