awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
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
pos :
  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 ⋯)) :
          α) :
      α)
pos₁ : 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 :
          α) :
      α)
have pos₂ : Membership.mem (α := α) (↑σ.support : Set α) ((σ : (a : α) → α) x : α)
Tactic: rw [Equiv.extendSubtype_apply_of_mem, Equiv.extendSubtype_apply_of_mem]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
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
⊢ 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 :
          α) :
      α)
have 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 :
    α)
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)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
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 :
      α)
⊢ 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 :
          α) :
      α)
have rwa : x ∉ (↑σ.support : Set α)
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)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
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 α)
⊢ 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 :
          α) :
      α)
have 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 :
    α)
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)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (hypothesis)
Goal:
α : Type u
s : Finset α
f : Perm α
h : ∀ x ∈ s, Membership.mem (α := α) s ((f : (a : α) → α) x : α)
y : α
hy : y ∈ s
⊢ Membership.mem (α := α) s ((Equiv.symm f : (a : α) → α) y : α)
have h0 : ∀ 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
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
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
⊢ Membership.mem (α := α) s ((Equiv.symm f : (a : α) → α) y : α)
have 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) : α)
Tactic: obtain ⟨y2, hy2, rfl⟩ := h0 y hy
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
f : Perm α
s : Set α
inst : Finite.{u + 1} (↑s : Type u)
h : Set.MapsTo (⇑f : (a : α) → α) s s
⊢ Set.MapsTo (⇑(Equiv.symm f) : (a : α) → α) s s
have intro : ∀ (val : Fintype (↑s : Type u)), Set.MapsTo (⇑(Equiv.symm f) : (a : α) → α) s s
Tactic: cases nonempty_fintype s
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
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
⊢ p ((Equiv.symm f : (a : α) → α) x)
have have : ∀ (this : Finite.{u + 1} (↑{x : α | p x} : Type u)), p ((Equiv.symm f : (a : α) → α) x)
Tactic: have : Finite { x | p x } := by simpa
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
m : Type u_1
n : Type u_2
inst : Finite m
inst_1 : Finite n
σ : Perm (m ⊕ n)
⊢ 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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
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)
⊢ 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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (hypothesis)
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) (⇑σ : (a : m ⊕ n) → m ⊕ n) (Set.range Sum.inr) (Set.range Sum.inr)
have h₁ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
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
⊢ 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)
have 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)
Tactic: rcases hx : σ x with l | r
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
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)
⊢ 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)
have 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)
Tactic: rcases hx : σ x with l | r
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
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) (⇑σ : (a : m ⊕ n) → m ⊕ n) (Set.range Sum.inr) (Set.range Sum.inr)
have 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)
Tactic: classical
        rw [← perm_symm_mapsTo_iff_mapsTo] at h
        intro x
        rcases hx : σ x with l | r
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
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)
⊢ Set.MapsTo (α := m ⊕ n) (β := m ⊕ n) (⇑σ : (a : m ⊕ n) → m ⊕ n) (Set.range Sum.inr) (Set.range Sum.inr)
have 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)
Tactic: classical
        rw [← perm_symm_mapsTo_iff_mapsTo] at h
        intro x
        rcases hx : σ x with l | r
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (hypothesis)
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) (⇑σ : (a : m ⊕ n) → m ⊕ n) (Set.range Sum.inl) (Set.range Sum.inl)
have h₁ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
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
⊢ 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)
have 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)
Tactic: rcases hx : σ x with l | r
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
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)
⊢ 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)
have 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)
Tactic: rcases hx : σ x with l | r
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
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) (⇑σ : (a : m ⊕ n) → m ⊕ n) (Set.range Sum.inl) (Set.range Sum.inl)
have 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)
Tactic: classical
        rw [← perm_symm_mapsTo_iff_mapsTo] at h
        intro x
        rcases hx : σ x with l | r
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
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)
⊢ Set.MapsTo (α := m ⊕ n) (β := m ⊕ n) (⇑σ : (a : m ⊕ n) → m ⊕ n) (Set.range Sum.inl) (Set.range Sum.inl)
have 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)
Tactic: classical
        rw [← perm_symm_mapsTo_iff_mapsTo] at h
        intro x
        rcases hx : σ x with l | r
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
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)
⊢ Membership.mem (γ := Set (m ⊕ n)) (Set.range Sum.inr) (Sum.inl l)
have 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)
Tactic: obtain ⟨y, hy⟩ := h ⟨l, rfl⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
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)
⊢ Membership.mem (γ := Set (m ⊕ n)) (Set.range Sum.inl) (Sum.inr r)
have 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)
Tactic: obtain ⟨y, hy⟩ := h ⟨r, rfl⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (hypothesis)
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)
⊢ σ ∈ (sumCongrHom m n).range
have h1 : ∀ (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⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (hypothesis)
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)
⊢ σ ∈ (sumCongrHom m n).range
have h3 : ∀ (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⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
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) σ₂'
⊢ σ ∈ (sumCongrHom m n).range
have rw : ∃ (a : Perm m) (b : Perm n), (sumCongrHom m n : (a : Perm m × Perm n) → Perm (m ⊕ n)) (a, b) = σ
Tactic: rw [MonoidHom.mem_range, Prod.exists]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
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) σ₂'
⊢ ∃ (a : Perm m) (b : Perm n), (sumCongrHom m n : (a : Perm m × Perm n) → Perm (m ⊕ n)) (a, b) = σ
have h₁ : (sumCongrHom m n : (a : Perm m × Perm n) → Perm (m ⊕ n)) (σ₁, σ₂) = σ
Tactic: use σ₁, σ₂