awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
σ τ : Perm α
f : { x : α // x ∈ (↑σ.support : Set α) } ≃ { x : α // x ∈ (↑τ.support : Set α) }
hf :
  ∀ (x : α) (hx : x ∈ (↑σ.support : Set α)),
    Eq (α := α)
      ((↑((f : (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
              (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) ((σ : (a : α) → α) x) ⋯)) :
          α) :
        α)
      ((τ : (a : α) → α)
          (↑((f : (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
                (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) x hx)) :
            α) :
        α)
x : α
hx : x ∉ σ.support
neg :
  Eq (α := α)
    ((f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)) :
          (a : α) → α)
        ((σ : (a : α) → α) x : α) :
      α)
    ((f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)) :
          (a : α) → α)
        x :
      α)
rwa : x ∉ (↑σ.support : Set α)
neg₁ :
  Eq (α := α)
    ((f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)) :
          (a : α) → α)
        x :
      α)
    ((f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)) :
          (a : α) → α)
        x :
      α)
rwa₁ : x ∉ (↑σ.support : Set α)
neg₂ :
  Eq (α := α)
    ((f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)) :
          (a : α) → α)
        x :
      α)
    ((f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)) :
          (a : α) → α)
        x :
      α)
rwa₂ rwa₃ rwa₄ : x ∉ (↑σ.support : Set α)
⊢ Eq (α := α)
    ((f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)) :
          (a : α) → α)
        ((σ : (a : α) → α) x : α) :
      α)
    ((τ : (a : α) → α)
        ((f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)) :
              (a : α) → α)
            x :
          α) :
      α)

Tactic:
rwa [Classical.not_not.1 ((not_congr mem_support).1 (Equiv.extendSubtype_not_mem f _ _)),
      Classical.not_not.1 ((not_congr mem_support).mp hx)]

Premises used: Classical.not_not, Equiv.Perm.mem_support, Equiv.extendSubtype_not_mem, Iff.mp, not_congr
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
s : Finset α
f : Perm α
h : ∀ x ∈ s, Membership.mem (α := α) s ((f : (a : α) → α) x : α)
y : α
hy : y ∈ s
⊢ ∀ y ∈ s, ∃ (x : α) (hx : x ∈ s), y = (fun (i : α) (x : i ∈ s) ↦ ((f : (a : α) → α) i : α)) x hx

Tactic:
have h0 : ∀ y ∈ s, ∃ (x : _) (hx : x ∈ s), y = (fun i (_ : i ∈ s) => f i) x hx :=
    Finset.surj_on_of_inj_on_of_card_le (fun x hx => (fun i _ => f i) x hx) (fun a ha => h a ha)
      (fun a₁ a₂ ha₁ ha₂ heq => (Equiv.apply_eq_iff_eq f).mp heq) rfl.ge
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
s : Finset α
f : Perm α
h : ∀ x ∈ s, Membership.mem (α := α) s ((f : (a : α) → α) x : α)
y : α
hy : y ∈ s
h0 : ∀ y ∈ s, ∃ (x : α) (hx : x ∈ s), y = (fun (i : α) (x : i ∈ s) ↦ ((f : (a : α) → α) i : α)) x hx
obtain :
  ∀ (y2 : α) (hy2 : y2 ∈ s) (hy : (fun (i : α) (x : i ∈ s) ↦ ((f : (a : α) → α) i : α)) y2 hy2 ∈ s),
    Membership.mem (α := α) s
      ((Equiv.symm f : (a : α) → α) ((fun (i : α) (x : i ∈ s) ↦ ((f : (a : α) → α) i : α)) y2 hy2) : α)
⊢ Membership.mem (α := α) s ((Equiv.symm f : (a : α) → α) y : α)

Tactic:
obtain ⟨y2, hy2, rfl⟩ := h0 y hy

Premises used: rfl
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
s : Finset α
f : Perm α
h : ∀ x ∈ s, Membership.mem (α := α) s ((f : (a : α) → α) x : α)
h0 : ∀ y ∈ s, ∃ (x : α) (hx : x ∈ s), y = (fun (i : α) (x : i ∈ s) ↦ ((f : (a : α) → α) i : α)) x hx
y2 : α
hy2 : y2 ∈ s
hy : (fun (i : α) (x : i ∈ s) ↦ ((f : (a : α) → α) i : α)) y2 hy2 ∈ s
⊢ Membership.mem (α := α) s
    ((Equiv.symm f : (a : α) → α) ((fun (i : α) (x : i ∈ s) ↦ ((f : (a : α) → α) i : α)) y2 hy2) : α)

Tactic:
simpa using hy2
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
f : Perm α
s : Set α
inst : Finite.{u + 1} (↑s : Type u)
h : Set.MapsTo (⇑f : (a : α) → α) s s
intro : ∀ (val : Fintype (↑s : Type u)), Set.MapsTo (⇑(Equiv.symm f) : (a : α) → α) s s
⊢ Set.MapsTo (⇑(Equiv.symm f) : (a : α) → α) s s

Tactic:
cases nonempty_fintype s

Premises used: Set.Elem, nonempty_fintype
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
f : Perm α
s : Set α
inst : Finite.{u + 1} (↑s : Type u)
h : Set.MapsTo (⇑f : (a : α) → α) s s
val : Fintype (↑s : Type u)
⊢ Set.MapsTo (⇑(Equiv.symm f) : (a : α) → α) s s

Tactic:
fun x hx =>
    Set.mem_toFinset.mp <|
      perm_symm_on_of_perm_on_finset
        (fun a ha => Set.mem_toFinset.mpr (h (Set.mem_toFinset.mp ha)))
        (Set.mem_toFinset.mpr hx)

Premises used: Iff.mpr, Equiv.Perm.perm_symm_on_of_perm_on_finset, Set.MapsTo, Iff.mp, Set.mem_toFinset
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
f : Perm α
s : Set α
inst : Finite.{u + 1} (↑s : Type u)
h : Set.MapsTo (⇑f : (a : α) → α) s s
val : Fintype (↑s : Type u)
⊢ Set.MapsTo (⇑(Equiv.symm f) : (a : α) → α) s s

Tactic:
exact fun x hx =>
    Set.mem_toFinset.mp <|
      perm_symm_on_of_perm_on_finset
        (fun a ha => Set.mem_toFinset.mpr (h (Set.mem_toFinset.mp ha)))
        (Set.mem_toFinset.mpr hx)

Premises used: Iff.mpr, Equiv.Perm.perm_symm_on_of_perm_on_finset, Iff.mp, Set.mem_toFinset
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
f : Perm α
s : Set α
inst : Finite.{u + 1} (↑s : Type u)
⊢ Set.MapsTo (⇑(Equiv.symm f) : (a : α) → α) s s ↔ Set.MapsTo (⇑f : (a : α) → α) s s

Tactic:
⟨perm_symm_mapsTo_of_mapsTo f⁻¹, perm_symm_mapsTo_of_mapsTo f⟩

Premises used: Inv.inv, Equiv.Perm.perm_symm_mapsTo_of_mapsTo, Iff.intro
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
f : Perm α
p : α → Prop
inst : Finite.{max 1 (u + 1)} { x : α // p x }
h : ∀ (x : α), p x → p ((f : (a : α) → α) x)
x : α
hx : p x
⊢ Finite.{u + 1} (↑{x : α | p x} : Type u)

Tactic:
simpa
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
f : Perm α
p : α → Prop
inst : Finite.{max 1 (u + 1)} { x : α // p x }
h : ∀ (x : α), p x → p ((f : (a : α) → α) x)
x : α
hx : p x
have : ∀ (this : Finite.{u + 1} (↑{x : α | p x} : Type u)), p ((Equiv.symm f : (a : α) → α) x)
⊢ p ((Equiv.symm f : (a : α) → α) x)

Tactic:
have : Finite { x | p x } := by simpa
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
f : Perm α
p : α → Prop
inst : Finite.{max 1 (u + 1)} { x : α // p x }
h : ∀ (x : α), p x → p ((f : (a : α) → α) x)
x : α
hx : p x
this : Finite.{u + 1} (↑{x : α | p x} : Type u)
⊢ p ((Equiv.symm f : (a : α) → α) x)

Tactic:
simpa using perm_symm_mapsTo_of_mapsTo (s := {x | p x}) f h hx

Premises used: Equiv.Perm.perm_symm_mapsTo_of_mapsTo
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
f : Perm α
p : α → Prop
inst : Finite.{max 1 (u + 1)} { x : α // p x }
h : ∀ (x : α), p x → p ((f : (a : α) → α) x)
x : { x : α // p x }
⊢ Eq (α := { x : α // p x })
    ((f.subtypePermOfFintype (p := p) h : (a : { x : α // p x }) → { x : α // p x }) x : { x : α // p x })
    (Subtype.mk (p := fun (x : α) ↦ p x) ((f : (a : α) → α) (↑x : α)) ⋯ : { x : α // p x })

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
p : α → Prop
inst : Finite.{max 1 (u + 1)} { x : α // p x }
h : ∀ (x : α), p x → p ((1 : (a : α) → α) x)
⊢ subtypePermOfFintype 1 (p := p) h = 1

Tactic:
rfl

Premises used: Equiv.Perm.subtypePerm, Equiv.refl, rfl
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
m : Type u_1
n : Type u_2
inst : Finite m
inst_1 : Finite n
σ : Perm (m ⊕ n)
mp :
  Set.MapsTo (α := m ⊕ n) (β := m ⊕ n) (⇑σ : (a : m ⊕ n) → m ⊕ n) (Set.range Sum.inl) (Set.range Sum.inl) →
    Set.MapsTo (α := m ⊕ n) (β := m ⊕ n) (⇑σ : (a : m ⊕ n) → m ⊕ n) (Set.range Sum.inr) (Set.range Sum.inr)
mpr :
  Set.MapsTo (α := m ⊕ n) (β := m ⊕ n) (⇑σ : (a : m ⊕ n) → m ⊕ n) (Set.range Sum.inr) (Set.range Sum.inr) →
    Set.MapsTo (α := m ⊕ n) (β := m ⊕ n) (⇑σ : (a : m ⊕ n) → m ⊕ n) (Set.range Sum.inl) (Set.range Sum.inl)
⊢ Set.MapsTo (α := m ⊕ n) (β := m ⊕ n) (⇑σ : (a : m ⊕ n) → m ⊕ n) (Set.range Sum.inl) (Set.range Sum.inl) ↔
    Set.MapsTo (α := m ⊕ n) (β := m ⊕ n) (⇑σ : (a : m ⊕ n) → m ⊕ n) (Set.range Sum.inr) (Set.range Sum.inr)

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
m : Type u_1
n : Type u_2
inst : Finite m
inst_1 : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (α := m ⊕ n) (β := m ⊕ n) (⇑σ : (a : m ⊕ n) → m ⊕ n) (Set.range Sum.inl) (Set.range Sum.inl)
⊢ Set.MapsTo (α := m ⊕ n) (β := m ⊕ n) (⇑(Equiv.symm σ) : (a : m ⊕ n) → m ⊕ n) (Set.range Sum.inl) (Set.range Sum.inl)

Tactic:
rw [← perm_symm_mapsTo_iff_mapsTo] at h

Premises used: Equiv.Perm.perm_symm_mapsTo_iff_mapsTo
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
m : Type u_1
n : Type u_2
inst : Finite m
inst_1 : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (α := m ⊕ n) (β := m ⊕ n) (⇑(Equiv.symm σ) : (a : m ⊕ n) → m ⊕ n) (Set.range Sum.inl) (Set.range Sum.inl)
x : m ⊕ n
mp :
  ∀ (l : m) (hx : Eq (α := m ⊕ n) ((σ : (a : m ⊕ n) → m ⊕ n) x : m ⊕ n) (Sum.inl l : m ⊕ n)),
    Membership.mem (γ := Set (m ⊕ n)) (Set.range Sum.inr) x →
      Membership.mem (γ := Set (m ⊕ n)) (Set.range Sum.inr) (Sum.inl l)
mp₁ :
  ∀ (r : n) (hx : Eq (α := m ⊕ n) ((σ : (a : m ⊕ n) → m ⊕ n) x : m ⊕ n) (Sum.inr r : m ⊕ n)),
    Membership.mem (γ := Set (m ⊕ n)) (Set.range Sum.inr) x →
      Membership.mem (γ := Set (m ⊕ n)) (Set.range Sum.inr) (Sum.inr r)
⊢ Membership.mem (γ := Set (m ⊕ n)) (Set.range Sum.inr) x →
    Membership.mem (α := m ⊕ n) (γ := Set (m ⊕ n)) (Set.range Sum.inr) ((σ : (a : m ⊕ n) → m ⊕ n) x : m ⊕ n)

Tactic:
rcases hx : σ x with l | r

Premises used: DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
m : Type u_1
n : Type u_2
inst : Finite m
inst_1 : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (α := m ⊕ n) (β := m ⊕ n) (⇑σ : (a : m ⊕ n) → m ⊕ n) (Set.range Sum.inl) (Set.range Sum.inl)
mp :
  ∀
    (h :
      Set.MapsTo (α := m ⊕ n) (β := m ⊕ n) (⇑(Equiv.symm σ) : (a : m ⊕ n) → m ⊕ n) (Set.range Sum.inl)
        (Set.range Sum.inl))
    ⦃x : m ⊕ n⦄ (l : m) (hx : Eq (α := m ⊕ n) ((σ : (a : m ⊕ n) → m ⊕ n) x : m ⊕ n) (Sum.inl l : m ⊕ n)),
    Membership.mem (γ := Set (m ⊕ n)) (Set.range Sum.inr) x →
      Membership.mem (γ := Set (m ⊕ n)) (Set.range Sum.inr) (Sum.inl l)
mp₁ :
  ∀
    (h :
      Set.MapsTo (α := m ⊕ n) (β := m ⊕ n) (⇑(Equiv.symm σ) : (a : m ⊕ n) → m ⊕ n) (Set.range Sum.inl)
        (Set.range Sum.inl))
    ⦃x : m ⊕ n⦄ (r : n) (hx : Eq (α := m ⊕ n) ((σ : (a : m ⊕ n) → m ⊕ n) x : m ⊕ n) (Sum.inr r : m ⊕ n)),
    Membership.mem (γ := Set (m ⊕ n)) (Set.range Sum.inr) x →
      Membership.mem (γ := Set (m ⊕ n)) (Set.range Sum.inr) (Sum.inr r)
⊢ Set.MapsTo (α := m ⊕ n) (β := m ⊕ n) (⇑σ : (a : m ⊕ n) → m ⊕ n) (Set.range Sum.inr) (Set.range Sum.inr)

Tactic:
classical
        rw [← perm_symm_mapsTo_iff_mapsTo] at h
        intro x
        rcases hx : σ x with l | r

Premises used: Equiv.Perm.perm_symm_mapsTo_iff_mapsTo
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
m : Type u_1
n : Type u_2
inst : Finite m
inst_1 : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (α := m ⊕ n) (β := m ⊕ n) (⇑σ : (a : m ⊕ n) → m ⊕ n) (Set.range Sum.inr) (Set.range Sum.inr)
⊢ Set.MapsTo (α := m ⊕ n) (β := m ⊕ n) (⇑(Equiv.symm σ) : (a : m ⊕ n) → m ⊕ n) (Set.range Sum.inr) (Set.range Sum.inr)

Tactic:
rw [← perm_symm_mapsTo_iff_mapsTo] at h

Premises used: Equiv.Perm.perm_symm_mapsTo_iff_mapsTo
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
m : Type u_1
n : Type u_2
inst : Finite m
inst_1 : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (α := m ⊕ n) (β := m ⊕ n) (⇑(Equiv.symm σ) : (a : m ⊕ n) → m ⊕ n) (Set.range Sum.inr) (Set.range Sum.inr)
x : m ⊕ n
mpr :
  ∀ (l : m) (hx : Eq (α := m ⊕ n) ((σ : (a : m ⊕ n) → m ⊕ n) x : m ⊕ n) (Sum.inl l : m ⊕ n)),
    Membership.mem (γ := Set (m ⊕ n)) (Set.range Sum.inl) x →
      Membership.mem (γ := Set (m ⊕ n)) (Set.range Sum.inl) (Sum.inl l)
mpr₁ :
  ∀ (r : n) (hx : Eq (α := m ⊕ n) ((σ : (a : m ⊕ n) → m ⊕ n) x : m ⊕ n) (Sum.inr r : m ⊕ n)),
    Membership.mem (γ := Set (m ⊕ n)) (Set.range Sum.inl) x →
      Membership.mem (γ := Set (m ⊕ n)) (Set.range Sum.inl) (Sum.inr r)
⊢ Membership.mem (γ := Set (m ⊕ n)) (Set.range Sum.inl) x →
    Membership.mem (α := m ⊕ n) (γ := Set (m ⊕ n)) (Set.range Sum.inl) ((σ : (a : m ⊕ n) → m ⊕ n) x : m ⊕ n)

Tactic:
rcases hx : σ x with l | r

Premises used: DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
m : Type u_1
n : Type u_2
inst : Finite m
inst_1 : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (α := m ⊕ n) (β := m ⊕ n) (⇑σ : (a : m ⊕ n) → m ⊕ n) (Set.range Sum.inr) (Set.range Sum.inr)
mpr :
  ∀
    (h :
      Set.MapsTo (α := m ⊕ n) (β := m ⊕ n) (⇑(Equiv.symm σ) : (a : m ⊕ n) → m ⊕ n) (Set.range Sum.inr)
        (Set.range Sum.inr))
    ⦃x : m ⊕ n⦄ (l : m) (hx : Eq (α := m ⊕ n) ((σ : (a : m ⊕ n) → m ⊕ n) x : m ⊕ n) (Sum.inl l : m ⊕ n)),
    Membership.mem (γ := Set (m ⊕ n)) (Set.range Sum.inl) x →
      Membership.mem (γ := Set (m ⊕ n)) (Set.range Sum.inl) (Sum.inl l)
mpr₁ :
  ∀
    (h :
      Set.MapsTo (α := m ⊕ n) (β := m ⊕ n) (⇑(Equiv.symm σ) : (a : m ⊕ n) → m ⊕ n) (Set.range Sum.inr)
        (Set.range Sum.inr))
    ⦃x : m ⊕ n⦄ (r : n) (hx : Eq (α := m ⊕ n) ((σ : (a : m ⊕ n) → m ⊕ n) x : m ⊕ n) (Sum.inr r : m ⊕ n)),
    Membership.mem (γ := Set (m ⊕ n)) (Set.range Sum.inl) x →
      Membership.mem (γ := Set (m ⊕ n)) (Set.range Sum.inl) (Sum.inr r)
⊢ Set.MapsTo (α := m ⊕ n) (β := m ⊕ n) (⇑σ : (a : m ⊕ n) → m ⊕ n) (Set.range Sum.inl) (Set.range Sum.inl)

Tactic:
classical
        rw [← perm_symm_mapsTo_iff_mapsTo] at h
        intro x
        rcases hx : σ x with l | r

Premises used: Equiv.Perm.perm_symm_mapsTo_iff_mapsTo
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
m : Type u_1
n : Type u_2
inst : Finite m
inst_1 : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (α := m ⊕ n) (β := m ⊕ n) (⇑(Equiv.symm σ) : (a : m ⊕ n) → m ⊕ n) (Set.range Sum.inl) (Set.range Sum.inl)
l : m
a : n
hx : Eq (α := m ⊕ n) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inr a) : m ⊕ n) (Sum.inl l : m ⊕ n)
mp :
  ∀ (y : m) (hy : Eq (α := m ⊕ n) (Sum.inl y) ((Equiv.symm σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl l))),
    Membership.mem (γ := Set (m ⊕ n)) (Set.range Sum.inr) (Sum.inl l)
⊢ Membership.mem (γ := Set (m ⊕ n)) (Set.range Sum.inr) (Sum.inl l)

Tactic:
obtain ⟨y, hy⟩ := h ⟨l, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
m : Type u_1
n : Type u_2
inst : Finite m
inst_1 : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (α := m ⊕ n) (β := m ⊕ n) (⇑(Equiv.symm σ) : (a : m ⊕ n) → m ⊕ n) (Set.range Sum.inl) (Set.range Sum.inl)
l : m
a : n
hx : Eq (α := m ⊕ n) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inr a) : m ⊕ n) (Sum.inl l : m ⊕ n)
y : m
hy : Eq (α := m ⊕ n) (Sum.inl y) ((Equiv.symm σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl l))
⊢ Membership.mem (γ := Set (m ⊕ n)) (Set.range Sum.inr) (Sum.inl l)

Tactic:
grind
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
m : Type u_1
n : Type u_2
inst : Finite m
inst_1 : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (α := m ⊕ n) (β := m ⊕ n) (⇑(Equiv.symm σ) : (a : m ⊕ n) → m ⊕ n) (Set.range Sum.inl) (Set.range Sum.inl)
x : m ⊕ n
r : n
hx : Eq (α := m ⊕ n) ((σ : (a : m ⊕ n) → m ⊕ n) x : m ⊕ n) (Sum.inr r : m ⊕ n)
h_1 : Membership.mem (γ := Set (m ⊕ n)) (Set.range Sum.inr) x
⊢ Membership.mem (γ := Set (m ⊕ n)) (Set.range Sum.inr) (Sum.inr r)

Tactic:
⟨r, rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range, rfl
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
m : Type u_1
n : Type u_2
inst : Finite m
inst_1 : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (α := m ⊕ n) (β := m ⊕ n) (⇑(Equiv.symm σ) : (a : m ⊕ n) → m ⊕ n) (Set.range Sum.inl) (Set.range Sum.inl)
x : m ⊕ n
r : n
hx : Eq (α := m ⊕ n) ((σ : (a : m ⊕ n) → m ⊕ n) x : m ⊕ n) (Sum.inr r : m ⊕ n)
h_1 : Membership.mem (γ := Set (m ⊕ n)) (Set.range Sum.inr) x
⊢ Membership.mem (γ := Set (m ⊕ n)) (Set.range Sum.inr) (Sum.inr r)

Tactic:
exact ⟨r, rfl⟩
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
m : Type u_1
n : Type u_2
inst : Finite m
inst_1 : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (α := m ⊕ n) (β := m ⊕ n) (⇑(Equiv.symm σ) : (a : m ⊕ n) → m ⊕ n) (Set.range Sum.inr) (Set.range Sum.inr)
x : m ⊕ n
l : m
hx : Eq (α := m ⊕ n) ((σ : (a : m ⊕ n) → m ⊕ n) x : m ⊕ n) (Sum.inl l : m ⊕ n)
h_1 : Membership.mem (γ := Set (m ⊕ n)) (Set.range Sum.inl) x
⊢ Membership.mem (γ := Set (m ⊕ n)) (Set.range Sum.inl) (Sum.inl l)

Tactic:
⟨l, rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range, rfl
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
m : Type u_1
n : Type u_2
inst : Finite m
inst_1 : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (α := m ⊕ n) (β := m ⊕ n) (⇑(Equiv.symm σ) : (a : m ⊕ n) → m ⊕ n) (Set.range Sum.inr) (Set.range Sum.inr)
x : m ⊕ n
l : m
hx : Eq (α := m ⊕ n) ((σ : (a : m ⊕ n) → m ⊕ n) x : m ⊕ n) (Sum.inl l : m ⊕ n)
h_1 : Membership.mem (γ := Set (m ⊕ n)) (Set.range Sum.inl) x
⊢ Membership.mem (γ := Set (m ⊕ n)) (Set.range Sum.inl) (Sum.inl l)

Tactic:
exact ⟨l, rfl⟩
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
m : Type u_1
n : Type u_2
inst : Finite m
inst_1 : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (α := m ⊕ n) (β := m ⊕ n) (⇑(Equiv.symm σ) : (a : m ⊕ n) → m ⊕ n) (Set.range Sum.inr) (Set.range Sum.inr)
r : n
a : m
hx : Eq (α := m ⊕ n) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a) : m ⊕ n) (Sum.inr r : m ⊕ n)
mpr :
  ∀ (y : n) (hy : Eq (α := m ⊕ n) (Sum.inr y) ((Equiv.symm σ : (a : m ⊕ n) → m ⊕ n) (Sum.inr r))),
    Membership.mem (γ := Set (m ⊕ n)) (Set.range Sum.inl) (Sum.inr r)
⊢ Membership.mem (γ := Set (m ⊕ n)) (Set.range Sum.inl) (Sum.inr r)

Tactic:
obtain ⟨y, hy⟩ := h ⟨r, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
m : Type u_1
n : Type u_2
inst : Finite m
inst_1 : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (α := m ⊕ n) (β := m ⊕ n) (⇑(Equiv.symm σ) : (a : m ⊕ n) → m ⊕ n) (Set.range Sum.inr) (Set.range Sum.inr)
r : n
a : m
hx : Eq (α := m ⊕ n) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a) : m ⊕ n) (Sum.inr r : m ⊕ n)
y : n
hy : Eq (α := m ⊕ n) (Sum.inr y) ((Equiv.symm σ : (a : m ⊕ n) → m ⊕ n) (Sum.inr r))
⊢ Membership.mem (γ := Set (m ⊕ n)) (Set.range Sum.inl) (Sum.inr r)

Tactic:
grind
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
m : Type u_1
n : Type u_2
inst : Finite m
inst_1 : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (α := m ⊕ n) (β := m ⊕ n) (⇑σ : (a : m ⊕ n) → m ⊕ n) (Set.range Sum.inl) (Set.range Sum.inl)
a : m
⊢ ∃ (a_1 : m), Eq (α := m ⊕ n) (Sum.inl a_1) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a))

Tactic:
h ⟨a, rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range, rfl
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
m : Type u_1
n : Type u_2
inst : Finite m
inst_1 : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (α := m ⊕ n) (β := m ⊕ n) (⇑σ : (a : m ⊕ n) → m ⊕ n) (Set.range Sum.inl) (Set.range Sum.inl)
a : m
⊢ ∃ (a_1 : m), Eq (α := m ⊕ n) (Sum.inl a_1) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a))

Tactic:
exact h ⟨a, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
m : Type u_1
n : Type u_2
inst : Finite m
inst_1 : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (α := m ⊕ n) (β := m ⊕ n) (⇑σ : (a : m ⊕ n) → m ⊕ n) (Set.range Sum.inl) (Set.range Sum.inl)
⊢ ∀ (x : m ⊕ n), (∃ (a : m), Sum.inl a = x) → ∃ (a : m), Eq (α := m ⊕ n) (Sum.inl a) ((σ : (a : m ⊕ n) → m ⊕ n) x)

Tactic:
have h1 : ∀ x : m ⊕ n, (∃ a : m, Sum.inl a = x) → ∃ a : m, Sum.inl a = σ x := by
    rintro _ ⟨a, rfl⟩; exact h ⟨a, rfl⟩
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
m : Type u_1
n : Type u_2
inst : Finite m
inst_1 : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (α := m ⊕ n) (β := m ⊕ n) (⇑σ : (a : m ⊕ n) → m ⊕ n) (Set.range Sum.inl) (Set.range Sum.inl)
h1 : ∀ (x : m ⊕ n), (∃ (a : m), Sum.inl a = x) → ∃ (a : m), Eq (α := m ⊕ n) (Sum.inl a) ((σ : (a : m ⊕ n) → m ⊕ n) x)
b : n
⊢ ∃ (b_1 : n), Eq (α := m ⊕ n) (Sum.inr b_1) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inr b))

Tactic:
(perm_mapsTo_inl_iff_mapsTo_inr σ).mp h ⟨b, rfl⟩

Premises used: Set.Mem, setOf, Equiv.Perm.perm_mapsTo_inl_iff_mapsTo_inr, Exists.intro, Iff.mp, Set.range, rfl
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
m : Type u_1
n : Type u_2
inst : Finite m
inst_1 : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (α := m ⊕ n) (β := m ⊕ n) (⇑σ : (a : m ⊕ n) → m ⊕ n) (Set.range Sum.inl) (Set.range Sum.inl)
h1 : ∀ (x : m ⊕ n), (∃ (a : m), Sum.inl a = x) → ∃ (a : m), Eq (α := m ⊕ n) (Sum.inl a) ((σ : (a : m ⊕ n) → m ⊕ n) x)
b : n
⊢ ∃ (b_1 : n), Eq (α := m ⊕ n) (Sum.inr b_1) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inr b))

Tactic:
exact (perm_mapsTo_inl_iff_mapsTo_inr σ).mp h ⟨b, rfl⟩

Premises used: Equiv.Perm.perm_mapsTo_inl_iff_mapsTo_inr, Exists.intro, Iff.mp, rfl
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
m : Type u_1
n : Type u_2
inst : Finite m
inst_1 : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (α := m ⊕ n) (β := m ⊕ n) (⇑σ : (a : m ⊕ n) → m ⊕ n) (Set.range Sum.inl) (Set.range Sum.inl)
h1 : ∀ (x : m ⊕ n), (∃ (a : m), Sum.inl a = x) → ∃ (a : m), Eq (α := m ⊕ n) (Sum.inl a) ((σ : (a : m ⊕ n) → m ⊕ n) x)
⊢ ∀ (x : m ⊕ n), (∃ (b : n), Sum.inr b = x) → ∃ (b : n), Eq (α := m ⊕ n) (Sum.inr b) ((σ : (a : m ⊕ n) → m ⊕ n) x)

Tactic:
have h3 : ∀ x : m ⊕ n, (∃ b : n, Sum.inr b = x) → ∃ b : n, Sum.inr b = σ x := by
    rintro _ ⟨b, rfl⟩; exact (perm_mapsTo_inl_iff_mapsTo_inr σ).mp h ⟨b, rfl⟩
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
m : Type u_1
n : Type u_2
inst : Finite m
inst_1 : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (α := m ⊕ n) (β := m ⊕ n) (⇑σ : (a : m ⊕ n) → m ⊕ n) (Set.range Sum.inl) (Set.range Sum.inl)
h1 : ∀ (x : m ⊕ n), (∃ (a : m), Sum.inl a = x) → ∃ (a : m), Eq (α := m ⊕ n) (Sum.inl a) ((σ : (a : m ⊕ n) → m ⊕ n) x)
h3 : ∀ (x : m ⊕ n), (∃ (b : n), Sum.inr b = x) → ∃ (b : n), Eq (α := m ⊕ n) (Sum.inr b) ((σ : (a : m ⊕ n) → m ⊕ n) x)
σ₁' : Perm { x : m ⊕ n // ∃ (a : m), Sum.inl a = x } :=
  σ.subtypePermOfFintype (p := fun (x : m ⊕ n) ↦ ∃ (a : m), Sum.inl a = x) h1
σ₂' : Perm { x : m ⊕ n // ∃ (b : n), Sum.inr b = x } :=
  σ.subtypePermOfFintype (p := fun (x : m ⊕ n) ↦ ∃ (b : n), Sum.inr b = x) h3
σ₁ : Perm m :=
  (permCongr (Equiv.symm (ofInjective Sum.inl ⋯)) : (a : Perm (↑(Set.range Sum.inl) : Type (max u_2 u_1))) → Perm m) σ₁'
σ₂ : Perm n :=
  (permCongr (Equiv.symm (ofInjective Sum.inr ⋯)) : (a : Perm (↑(Set.range Sum.inr) : Type (max u_2 u_1))) → Perm n) σ₂'
rw : ∃ (a : Perm m) (b : Perm n), (sumCongrHom m n : (a : Perm m × Perm n) → Perm (m ⊕ n)) (a, b) = σ
⊢ σ ∈ (sumCongrHom m n).range

Tactic:
rw [MonoidHom.mem_range, Prod.exists]

Premises used: MonoidHom.mem_range, Prod.exists
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
m : Type u_1
n : Type u_2
inst : Finite m
inst_1 : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (α := m ⊕ n) (β := m ⊕ n) (⇑σ : (a : m ⊕ n) → m ⊕ n) (Set.range Sum.inl) (Set.range Sum.inl)
h1 : ∀ (x : m ⊕ n), (∃ (a : m), Sum.inl a = x) → ∃ (a : m), Eq (α := m ⊕ n) (Sum.inl a) ((σ : (a : m ⊕ n) → m ⊕ n) x)
h3 : ∀ (x : m ⊕ n), (∃ (b : n), Sum.inr b = x) → ∃ (b : n), Eq (α := m ⊕ n) (Sum.inr b) ((σ : (a : m ⊕ n) → m ⊕ n) x)
σ₁' : Perm { x : m ⊕ n // ∃ (a : m), Sum.inl a = x } :=
  σ.subtypePermOfFintype (p := fun (x : m ⊕ n) ↦ ∃ (a : m), Sum.inl a = x) h1
σ₂' : Perm { x : m ⊕ n // ∃ (b : n), Sum.inr b = x } :=
  σ.subtypePermOfFintype (p := fun (x : m ⊕ n) ↦ ∃ (b : n), Sum.inr b = x) h3
σ₁ : Perm m :=
  (permCongr (Equiv.symm (ofInjective Sum.inl ⋯)) : (a : Perm (↑(Set.range Sum.inl) : Type (max u_2 u_1))) → Perm m) σ₁'
σ₂ : Perm n :=
  (permCongr (Equiv.symm (ofInjective Sum.inr ⋯)) : (a : Perm (↑(Set.range Sum.inr) : Type (max u_2 u_1))) → Perm n) σ₂'
h₁ : (sumCongrHom m n : (a : Perm m × Perm n) → Perm (m ⊕ n)) (σ₁, σ₂) = σ
⊢ ∃ (a : Perm m) (b : Perm n), (sumCongrHom m n : (a : Perm m × Perm n) → Perm (m ⊕ n)) (a, b) = σ

Tactic:
use σ₁, σ₂