awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
β : Type v
p : β → Prop
inst : DecidablePred p
f : Equiv.{u + 1, max 1 (v + 1)} α (Subtype p)
σ τ : Perm α
h : σ.Disjoint τ
b : β
pb : p b
⊢ (σ.extendDomain (p := p) f : (a : β) → β) b = b ∨ (τ.extendDomain (p := p) f : (a : β) → β) b = b
have pos : Eq (α := α) ((σ : (a : α) → α) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b pb) : α) : α)
    ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b pb) : α) →
  (σ.extendDomain (p := p) f : (a : β) → β) b = b
Tactic: refine (h (f.symm ⟨b, pb⟩)).imp ?_ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
β : Type v
p : β → Prop
inst : DecidablePred p
f : Equiv.{u + 1, max 1 (v + 1)} α (Subtype p)
σ τ : Perm α
h : σ.Disjoint τ
b : β
pb : p b
pos :
  Eq (α := α) ((σ : (a : α) → α) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b pb) : α) : α)
      ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b pb) : α) →
    (σ.extendDomain (p := p) f : (a : β) → β) b = b
⊢ (σ.extendDomain (p := p) f : (a : β) → β) b = b ∨ (τ.extendDomain (p := p) f : (a : β) → β) b = b
have pos₁ : Eq (α := α) ((τ : (a : α) → α) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b pb) : α) : α)
    ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b pb) : α) →
  (τ.extendDomain (p := p) f : (a : β) → β) b = b
Tactic: refine (h (f.symm ⟨b, pb⟩)).imp ?_ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
β : Type v
p : β → Prop
inst : DecidablePred p
f : Equiv.{u + 1, max 1 (v + 1)} α (Subtype p)
σ τ : Perm α
h_1 : σ.Disjoint τ
b : β
pb : p b
h :
  Eq (α := α) ((σ : (a : α) → α) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b pb) : α) : α)
    ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b pb) : α)
⊢ (σ.extendDomain (p := p) f : (a : β) → β) b = b
have pos : (↑((f : (a : α) → Subtype p) ((σ : (a : α) → α) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b pb) : α))) : β) =
  b
Tactic: rw [extendDomain_apply_subtype _ _ pb, h, apply_symm_apply, Subtype.coe_mk]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
β : Type v
p : β → Prop
inst : DecidablePred p
f : Equiv.{u + 1, max 1 (v + 1)} α (Subtype p)
σ τ : Perm α
h_1 : σ.Disjoint τ
b : β
pb : p b
h :
  Eq (α := α) ((σ : (a : α) → α) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b pb) : α) : α)
    ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b pb) : α)
pos :
  (↑((f : (a : α) → Subtype p) ((σ : (a : α) → α) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b pb) : α))) :
      β) =
    b
⊢ (σ.extendDomain (p := p) f : (a : β) → β) b = b
have pos₁ : (↑((f : (a : α) → Subtype p) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b pb))) : β) = b
Tactic: rw [extendDomain_apply_subtype _ _ pb, h, apply_symm_apply, Subtype.coe_mk]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
β : Type v
p : β → Prop
inst : DecidablePred p
f : Equiv.{u + 1, max 1 (v + 1)} α (Subtype p)
σ τ : Perm α
h_1 : σ.Disjoint τ
b : β
pb : p b
h :
  Eq (α := α) ((σ : (a : α) → α) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b pb) : α) : α)
    ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b pb) : α)
pos :
  (↑((f : (a : α) → Subtype p) ((σ : (a : α) → α) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b pb) : α))) :
      β) =
    b
pos₁ : (↑((f : (a : α) → Subtype p) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b pb))) : β) = b
⊢ (σ.extendDomain (p := p) f : (a : β) → β) b = b
have pos₂ : (↑(Subtype.mk (p := p) b pb) : β) = b
Tactic: rw [extendDomain_apply_subtype _ _ pb, h, apply_symm_apply, Subtype.coe_mk]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
β : Type v
p : β → Prop
inst : DecidablePred p
f : Equiv.{u + 1, max 1 (v + 1)} α (Subtype p)
σ τ : Perm α
h_1 : σ.Disjoint τ
b : β
pb : p b
h :
  Eq (α := α) ((σ : (a : α) → α) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b pb) : α) : α)
    ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b pb) : α)
pos :
  (↑((f : (a : α) → Subtype p) ((σ : (a : α) → α) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b pb) : α))) :
      β) =
    b
pos₁ : (↑((f : (a : α) → Subtype p) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b pb))) : β) = b
pos₂ : (↑(Subtype.mk (p := p) b pb) : β) = b
⊢ (σ.extendDomain (p := p) f : (a : β) → β) b = b
have pos₃ : b = b
Tactic: rw [extendDomain_apply_subtype _ _ pb, h, apply_symm_apply, Subtype.coe_mk]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
β : Type v
p : β → Prop
inst : DecidablePred p
f : Equiv.{u + 1, max 1 (v + 1)} α (Subtype p)
σ τ : Perm α
h_1 : σ.Disjoint τ
b : β
pb : p b
h :
  Eq (α := α) ((τ : (a : α) → α) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b pb) : α) : α)
    ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b pb) : α)
⊢ (τ.extendDomain (p := p) f : (a : β) → β) b = b
have pos : (↑((f : (a : α) → Subtype p) ((τ : (a : α) → α) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b pb) : α))) : β) =
  b
Tactic: rw [extendDomain_apply_subtype _ _ pb, h, apply_symm_apply, Subtype.coe_mk]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
β : Type v
p : β → Prop
inst : DecidablePred p
f : Equiv.{u + 1, max 1 (v + 1)} α (Subtype p)
σ τ : Perm α
h_1 : σ.Disjoint τ
b : β
pb : p b
h :
  Eq (α := α) ((τ : (a : α) → α) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b pb) : α) : α)
    ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b pb) : α)
pos :
  (↑((f : (a : α) → Subtype p) ((τ : (a : α) → α) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b pb) : α))) :
      β) =
    b
⊢ (τ.extendDomain (p := p) f : (a : β) → β) b = b
have pos₁ : (↑((f : (a : α) → Subtype p) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b pb))) : β) = b
Tactic: rw [extendDomain_apply_subtype _ _ pb, h, apply_symm_apply, Subtype.coe_mk]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
β : Type v
p : β → Prop
inst : DecidablePred p
f : Equiv.{u + 1, max 1 (v + 1)} α (Subtype p)
σ τ : Perm α
h_1 : σ.Disjoint τ
b : β
pb : p b
h :
  Eq (α := α) ((τ : (a : α) → α) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b pb) : α) : α)
    ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b pb) : α)
pos :
  (↑((f : (a : α) → Subtype p) ((τ : (a : α) → α) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b pb) : α))) :
      β) =
    b
pos₁ : (↑((f : (a : α) → Subtype p) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b pb))) : β) = b
⊢ (τ.extendDomain (p := p) f : (a : β) → β) b = b
have pos₂ : (↑(Subtype.mk (p := p) b pb) : β) = b
Tactic: rw [extendDomain_apply_subtype _ _ pb, h, apply_symm_apply, Subtype.coe_mk]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
β : Type v
p : β → Prop
inst : DecidablePred p
f : Equiv.{u + 1, max 1 (v + 1)} α (Subtype p)
σ τ : Perm α
h_1 : σ.Disjoint τ
b : β
pb : p b
h :
  Eq (α := α) ((τ : (a : α) → α) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b pb) : α) : α)
    ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b pb) : α)
pos :
  (↑((f : (a : α) → Subtype p) ((τ : (a : α) → α) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b pb) : α))) :
      β) =
    b
pos₁ : (↑((f : (a : α) → Subtype p) ((f.symm : (a : Subtype p) → α) (Subtype.mk (p := p) b pb))) : β) = b
pos₂ : (↑(Subtype.mk (p := p) b pb) : β) = b
⊢ (τ.extendDomain (p := p) f : (a : β) → β) b = b
have pos₃ : b = b
Tactic: rw [extendDomain_apply_subtype _ _ pb, h, apply_symm_apply, Subtype.coe_mk]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
β : Type v
p : β → Prop
inst : DecidablePred p
f : Equiv.{u + 1, max 1 (v + 1)} α (Subtype p)
σ τ : Perm α
h : σ.Disjoint τ
b : β
pb : ¬p b
⊢ (σ.extendDomain (p := p) f : (a : β) → β) b = b ∨ (τ.extendDomain (p := p) f : (a : β) → β) b = b
have neg : (σ.extendDomain (p := p) f : (a : β) → β) b = b
Tactic: left
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
β : Type v
p : β → Prop
inst : DecidablePred p
f : Equiv.{u + 1, max 1 (v + 1)} α (Subtype p)
σ τ : Perm α
h : σ.Disjoint τ
b : β
pb : ¬p b
⊢ (σ.extendDomain (p := p) f : (a : β) → β) b = b
have neg : b = b
Tactic: rw [extendDomain_apply_not_subtype _ _ pb]
-- 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: cases nonempty_fintype α
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
inst : Finite α
σ τ π ρ : Perm α
hc1 : IsConj σ π
hc2 : IsConj τ ρ
hd1 : σ.Disjoint τ
hd2 : π.Disjoint ρ
val : Fintype α
⊢ IsConj (σ * τ) (π * ρ)
have intro : ∀ (f : Perm α) (hc1 : IsConj σ (f * σ * f⁻¹)) (hd2 : (f * σ * f⁻¹).Disjoint ρ), IsConj (σ * τ) (f * σ * f⁻¹ * ρ)
Tactic: obtain ⟨f, rfl⟩ := isConj_iff.1 hc1
Cleared hypotheses: π, hc1, hd2
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
inst : Finite α
σ τ ρ : Perm α
hc2 : IsConj τ ρ
hd1 : σ.Disjoint τ
val : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint ρ
⊢ IsConj (σ * τ) (f * σ * f⁻¹ * ρ)
have intro : ∀ (g : Perm α) (hc2 : IsConj τ (g * τ * g⁻¹)) (hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)),
  IsConj (σ * τ) (f * σ * f⁻¹ * (g * τ * g⁻¹))
Tactic: obtain ⟨g, rfl⟩ := isConj_iff.1 hc2
Cleared hypotheses: ρ, hc2, hd2
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (hypothesis)
Goal:
α : Type u
inst : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
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⁻¹))
have hd1' : (↑(σ * τ).support : Set α) = (↑(σ.support ∪ τ.support) : Set α)
Tactic: have hd1' := coe_inj.2 hd1.support_mul
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (hypothesis)
Goal:
α : Type u
inst : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : (↑(σ * τ).support : Set α) = (↑(σ.support ∪ τ.support) : Set α)
⊢ IsConj (σ * τ) (f * σ * f⁻¹ * (g * τ * g⁻¹))
have hd2' : (↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support : Set α) = (↑((f * σ * f⁻¹).support ∪ (g * τ * g⁻¹).support) : Set α)
Tactic: have hd2' := coe_inj.2 hd2.support_mul
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (hypothesis)
Goal:
α : Type u
inst : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : (↑(σ * τ).support : Set α) = (↑(σ.support ∪ τ.support) : Set α)
hd2' : (↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support : Set α) = (↑((f * σ * f⁻¹).support ∪ (g * τ * g⁻¹).support) : Set α)
⊢ IsConj (σ * τ) (f * σ * f⁻¹ * (g * τ * g⁻¹))
have hd1'₁ : (↑(σ * τ).support : Set α) = (↑σ.support : Set α) ∪ (↑τ.support : Set α)
Tactic: rw [coe_union] at *
Cleared hypotheses: hd1', hd2'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (hypothesis)
Goal:
α : Type u
inst : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : (↑(σ * τ).support : Set α) = (↑(σ.support ∪ τ.support) : Set α)
hd2' : (↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support : Set α) = (↑((f * σ * f⁻¹).support ∪ (g * τ * g⁻¹).support) : Set α)
hd1'₁ : (↑(σ * τ).support : Set α) = (↑σ.support : Set α) ∪ (↑τ.support : Set α)
⊢ IsConj (σ * τ) (f * σ * f⁻¹ * (g * τ * g⁻¹))
have hd2'₁ : (↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support : Set α) = (↑(f * σ * f⁻¹).support : Set α) ∪ (↑(g * τ * g⁻¹).support : Set α)
Tactic: rw [coe_union] at *
Cleared hypotheses: hd1', hd2'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (hypothesis)
Goal:
α : Type u
inst : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : (↑(σ * τ).support : Set α) = (↑σ.support : Set α) ∪ (↑τ.support : Set α)
hd2' :
  (↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support : Set α) = (↑(f * σ * f⁻¹).support : Set α) ∪ (↑(g * τ * g⁻¹).support : Set α)
⊢ IsConj (σ * τ) (f * σ * f⁻¹ * (g * τ * g⁻¹))
have hd1'' : _root_.Disjoint (↑σ.support : Set α) (↑τ.support : Set α)
Tactic: have hd1'' := disjoint_coe.2 (disjoint_iff_disjoint_support.1 hd1)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (hypothesis)
Goal:
α : Type u
inst : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : (↑(σ * τ).support : Set α) = (↑σ.support : Set α) ∪ (↑τ.support : Set α)
hd2' :
  (↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support : Set α) = (↑(f * σ * f⁻¹).support : Set α) ∪ (↑(g * τ * g⁻¹).support : Set α)
hd1'' : _root_.Disjoint (↑σ.support : Set α) (↑τ.support : Set α)
⊢ IsConj (σ * τ) (f * σ * f⁻¹ * (g * τ * g⁻¹))
have hd2'' : _root_.Disjoint (↑(f * σ * f⁻¹).support : Set α) (↑(g * τ * g⁻¹).support : Set α)
Tactic: have hd2'' := disjoint_coe.2 (disjoint_iff_disjoint_support.1 hd2)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
inst : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : (↑(σ * τ).support : Set α) = (↑σ.support : Set α) ∪ (↑τ.support : Set α)
hd2' :
  (↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support : Set α) = (↑(f * σ * f⁻¹).support : Set α) ∪ (↑(g * τ * g⁻¹).support : Set α)
hd1'' : _root_.Disjoint (↑σ.support : Set α) (↑τ.support : Set α)
hd2'' : _root_.Disjoint (↑(f * σ * f⁻¹).support : Set α) (↑(g * τ * g⁻¹).support : Set α)
⊢ IsConj (σ * τ) (f * σ * f⁻¹ * (g * τ * g⁻¹))
have intro : { x : α // x ∈ (↑(σ * τ).support : Set α) } ≃ { x : α // x ∈ (↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support : Set α) }
Tactic: refine isConj_of_support_equiv ?_ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
inst : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : (↑(σ * τ).support : Set α) = (↑σ.support : Set α) ∪ (↑τ.support : Set α)
hd2' :
  (↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support : Set α) = (↑(f * σ * f⁻¹).support : Set α) ∪ (↑(g * τ * g⁻¹).support : Set α)
hd1'' : _root_.Disjoint (↑σ.support : Set α) (↑τ.support : Set α)
hd2'' : _root_.Disjoint (↑(f * σ * f⁻¹).support : Set α) (↑(g * τ * g⁻¹).support : Set α)
⊢ { x : α // x ∈ (↑(σ * τ).support : Set α) } ≃ { x : α // x ∈ (↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support : Set α) }
have intro : ∀ (a : α), a ∈ (↑σ.support : Set α) ↔ Membership.mem (α := α) (↑(f * σ * f⁻¹).support : Set α) ((f : (a : α) → α) a : α)
Tactic: 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
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
inst : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : (↑(σ * τ).support : Set α) = (↑σ.support : Set α) ∪ (↑τ.support : Set α)
hd2' :
  (↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support : Set α) = (↑(f * σ * f⁻¹).support : Set α) ∪ (↑(g * τ * g⁻¹).support : Set α)
hd1'' : _root_.Disjoint (↑σ.support : Set α) (↑τ.support : Set α)
hd2'' : _root_.Disjoint (↑(f * σ * f⁻¹).support : Set α) (↑(g * τ * g⁻¹).support : Set α)
intro :
  ∀ (a : α),
    a ∈ (↑σ.support : Set α) ↔ Membership.mem (α := α) (↑(f * σ * f⁻¹).support : Set α) ((f : (a : α) → α) a : α)
⊢ { x : α // x ∈ (↑(σ * τ).support : Set α) } ≃ { x : α // x ∈ (↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support : Set α) }
have intro₁ : ∀ (a : α), a ∈ (↑τ.support : Set α) ↔ Membership.mem (α := α) (↑(g * τ * g⁻¹).support : Set α) ((g : (a : α) → α) a : α)
Tactic: 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
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
inst : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : (↑(σ * τ).support : Set α) = (↑σ.support : Set α) ∪ (↑τ.support : Set α)
hd2' :
  (↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support : Set α) = (↑(f * σ * f⁻¹).support : Set α) ∪ (↑(g * τ * g⁻¹).support : Set α)
hd1'' : _root_.Disjoint (↑σ.support : Set α) (↑τ.support : Set α)
hd2'' : _root_.Disjoint (↑(f * σ * f⁻¹).support : Set α) (↑(g * τ * g⁻¹).support : Set α)
x : α
hx : x ∈ (↑(σ * τ).support : Set α)
hxσ : (σ : (a : α) → α) x ≠ x
⊢ Eq (α := α) ((τ : (a : α) → α) x : α)
    ((Equiv.symm f : (a : α) → α)
        ((g : (a : α) → α) ((τ : (a : α) → α) ((Equiv.symm g : (a : α) → α) ((f : (a : α) → α) x : α) : α) : α) : α) :
      α)
have intro : ∀ (h : Eq (α := α) ((g * τ * g⁻¹ : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α)),
  Eq (α := α) ((τ : (a : α) → α) x : α)
    ((Equiv.symm f : (a : α) → α)
        ((g : (a : α) → α) ((τ : (a : α) → α) ((Equiv.symm g : (a : α) → α) ((f : (a : α) → α) x : α) : α) : α) : α) :
      α)
Tactic: have h := (hd2 (f x)).resolve_left ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
inst : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : (↑(σ * τ).support : Set α) = (↑σ.support : Set α) ∪ (↑τ.support : Set α)
hd2' :
  (↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support : Set α) = (↑(f * σ * f⁻¹).support : Set α) ∪ (↑(g * τ * g⁻¹).support : Set α)
hd1'' : _root_.Disjoint (↑σ.support : Set α) (↑τ.support : Set α)
hd2'' : _root_.Disjoint (↑(f * σ * f⁻¹).support : Set α) (↑(g * τ * g⁻¹).support : Set α)
x : α
hx : x ∈ (↑(σ * τ).support : Set α)
hxσ : (σ : (a : α) → α) x ≠ x
intro :
  ∀ (h : Eq (α := α) ((g * τ * g⁻¹ : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α)),
    Eq (α := α) ((τ : (a : α) → α) x : α)
      ((Equiv.symm f : (a : α) → α)
          ((g : (a : α) → α) ((τ : (a : α) → α) ((Equiv.symm g : (a : α) → α) ((f : (a : α) → α) x : α) : α) : α) : α) :
        α)
⊢ Eq (α := α) ((τ : (a : α) → α) x : α)
    ((Equiv.symm f : (a : α) → α)
        ((g : (a : α) → α) ((τ : (a : α) → α) ((Equiv.symm g : (a : α) → α) ((f : (a : α) → α) x : α) : α) : α) : α) :
      α)
have intro₁ : ¬Eq (α := α) ((f * σ * f⁻¹ : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α)
Tactic: have h := (hd2 (f x)).resolve_left ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (hypothesis)
Goal:
α : Type u
inst : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : (↑(σ * τ).support : Set α) = (↑σ.support : Set α) ∪ (↑τ.support : Set α)
hd2' :
  (↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support : Set α) = (↑(f * σ * f⁻¹).support : Set α) ∪ (↑(g * τ * g⁻¹).support : Set α)
hd1'' : _root_.Disjoint (↑σ.support : Set α) (↑τ.support : Set α)
hd2'' : _root_.Disjoint (↑(f * σ * f⁻¹).support : Set α) (↑(g * τ * g⁻¹).support : Set α)
x : α
hx : x ∈ (↑(σ * τ).support : Set α)
hxσ : (σ : (a : α) → α) x ≠ x
h : Eq (α := α) ((g * τ * g⁻¹ : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α)
⊢ Eq (α := α) ((τ : (a : α) → α) x : α)
    ((Equiv.symm f : (a : α) → α)
        ((g : (a : α) → α) ((τ : (a : α) → α) ((Equiv.symm g : (a : α) → α) ((f : (a : α) → α) x : α) : α) : α) : α) :
      α)
have h₁ : Eq (α := α) ((g : (a : α) → α) ((τ : (a : α) → α) ((Equiv.symm g : (a : α) → α) ((f : (a : α) → α) x : α) : α) : α) : α)
  ((f : (a : α) → α) x : α)
Tactic: rw [mul_apply, mul_apply, coe_inv] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
inst : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : (↑(σ * τ).support : Set α) = (↑σ.support : Set α) ∪ (↑τ.support : Set α)
hd2' :
  (↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support : Set α) = (↑(f * σ * f⁻¹).support : Set α) ∪ (↑(g * τ * g⁻¹).support : Set α)
hd1'' : _root_.Disjoint (↑σ.support : Set α) (↑τ.support : Set α)
hd2'' : _root_.Disjoint (↑(f * σ * f⁻¹).support : Set α) (↑(g * τ * g⁻¹).support : Set α)
x : α
hx : x ∈ (↑(σ * τ).support : Set α)
hxσ : (σ : (a : α) → α) x ≠ x
h :
  Eq (α := α)
    ((g : (a : α) → α) ((τ : (a : α) → α) ((Equiv.symm g : (a : α) → α) ((f : (a : α) → α) x : α) : α) : α) : α)
    ((f : (a : α) → α) x : α)
⊢ Eq (α := α) ((τ : (a : α) → α) x : α)
    ((Equiv.symm f : (a : α) → α)
        ((g : (a : α) → α) ((τ : (a : α) → α) ((Equiv.symm g : (a : α) → α) ((f : (a : α) → α) x : α) : α) : α) : α) :
      α)
have intro : Eq (α := α) ((τ : (a : α) → α) x : α) ((Equiv.symm f : (a : α) → α) ((f : (a : α) → α) x : α) : α)
Tactic: rw [h, symm_apply_apply, (hd1 x).resolve_left hxσ]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
inst : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : (↑(σ * τ).support : Set α) = (↑σ.support : Set α) ∪ (↑τ.support : Set α)
hd2' :
  (↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support : Set α) = (↑(f * σ * f⁻¹).support : Set α) ∪ (↑(g * τ * g⁻¹).support : Set α)
hd1'' : _root_.Disjoint (↑σ.support : Set α) (↑τ.support : Set α)
hd2'' : _root_.Disjoint (↑(f * σ * f⁻¹).support : Set α) (↑(g * τ * g⁻¹).support : Set α)
x : α
hx : x ∈ (↑(σ * τ).support : Set α)
hxσ : (σ : (a : α) → α) x ≠ x
h :
  Eq (α := α)
    ((g : (a : α) → α) ((τ : (a : α) → α) ((Equiv.symm g : (a : α) → α) ((f : (a : α) → α) x : α) : α) : α) : α)
    ((f : (a : α) → α) x : α)
intro : Eq (α := α) ((τ : (a : α) → α) x : α) ((Equiv.symm f : (a : α) → α) ((f : (a : α) → α) x : α) : α)
⊢ Eq (α := α) ((τ : (a : α) → α) x : α)
    ((Equiv.symm f : (a : α) → α)
        ((g : (a : α) → α) ((τ : (a : α) → α) ((Equiv.symm g : (a : α) → α) ((f : (a : α) → α) x : α) : α) : α) : α) :
      α)
have intro₁ : (τ : (a : α) → α) x = x
Tactic: rw [h, symm_apply_apply, (hd1 x).resolve_left hxσ]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
inst : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : (↑(σ * τ).support : Set α) = (↑σ.support : Set α) ∪ (↑τ.support : Set α)
hd2' :
  (↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support : Set α) = (↑(f * σ * f⁻¹).support : Set α) ∪ (↑(g * τ * g⁻¹).support : Set α)
hd1'' : _root_.Disjoint (↑σ.support : Set α) (↑τ.support : Set α)
hd2'' : _root_.Disjoint (↑(f * σ * f⁻¹).support : Set α) (↑(g * τ * g⁻¹).support : Set α)
x : α
hx : x ∈ (↑(σ * τ).support : Set α)
hxσ : (σ : (a : α) → α) x ≠ x
h :
  Eq (α := α)
    ((g : (a : α) → α) ((τ : (a : α) → α) ((Equiv.symm g : (a : α) → α) ((f : (a : α) → α) x : α) : α) : α) : α)
    ((f : (a : α) → α) x : α)
intro : Eq (α := α) ((τ : (a : α) → α) x : α) ((Equiv.symm f : (a : α) → α) ((f : (a : α) → α) x : α) : α)
intro₁ : (τ : (a : α) → α) x = x
⊢ Eq (α := α) ((τ : (a : α) → α) x : α)
    ((Equiv.symm f : (a : α) → α)
        ((g : (a : α) → α) ((τ : (a : α) → α) ((Equiv.symm g : (a : α) → α) ((f : (a : α) → α) x : α) : α) : α) : α) :
      α)
have intro₂ : x = x
Tactic: rw [h, symm_apply_apply, (hd1 x).resolve_left hxσ]