awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) σ₂'
⊢ (σ₁, σ₂).1.sumCongr (σ₁, σ₂).2 = σ
have h₁ : ∀ (a : m),
  Eq (α := m ⊕ n) (((σ₁, σ₂).1.sumCongr (σ₁, σ₂).2 : (a : m ⊕ n) → m ⊕ n) (Sum.inl a) : m ⊕ n)
    ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a) : m ⊕ n)
Tactic: ext (a | b)
-- 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) σ₂'
h₁ :
  ∀ (a : m),
    Eq (α := m ⊕ n) (((σ₁, σ₂).1.sumCongr (σ₁, σ₂).2 : (a : m ⊕ n) → m ⊕ n) (Sum.inl a) : m ⊕ n)
      ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a) : m ⊕ n)
⊢ (σ₁, σ₂).1.sumCongr (σ₁, σ₂).2 = σ
have h₂ : ∀ (b : n),
  Eq (α := m ⊕ n) (((σ₁, σ₂).1.sumCongr (σ₁, σ₂).2 : (a : m ⊕ n) → m ⊕ n) (Sum.inr b) : m ⊕ n)
    ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inr b) : m ⊕ n)
Tactic: ext (a | b)
-- 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 : m
⊢ Eq (α := m ⊕ n) (((σ₁, σ₂).1.sumCongr (σ₁, σ₂).2 : (a : m ⊕ n) → m ⊕ n) (Sum.inl a) : m ⊕ n)
    ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a) : m ⊕ n)
have h₁ : Eq (α := m ⊕ n)
  ((↑((σ₁' : (a : (↑(Set.range Sum.inl) : Type (max u_2 u_1))) → (↑(Set.range Sum.inl) : Type (max u_2 u_1)))
          ((ofInjective Sum.inl sorry : (a : m) → (↑(Set.range Sum.inl) : Type (max u_2 u_1))) a)) :
      m ⊕ n) :
    m ⊕ n)
  ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a) : m ⊕ n)
Tactic: rw [Equiv.sumCongr_apply, Sum.map_inl, permCongr_apply, Equiv.symm_symm,
      apply_ofInjective_symm Sum.inl_injective]
-- 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 : m
⊢ Eq (α := m ⊕ n)
    ((↑((σ₁' : (a : (↑(Set.range Sum.inl) : Type (max u_2 u_1))) → (↑(Set.range Sum.inl) : Type (max u_2 u_1)))
            ((ofInjective Sum.inl ⋯ : (a : m) → (↑(Set.range Sum.inl) : Type (max u_2 u_1))) a)) :
        m ⊕ n) :
      m ⊕ n)
    ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a) : m ⊕ n)
have h₁ : Eq (α := m ⊕ n)
  ((↑((σ₁' : (a : (↑(Set.range Sum.inl) : Type (max u_2 u_1))) → (↑(Set.range Sum.inl) : Type (max u_2 u_1)))
          (Subtype.mk (p := fun (x : m ⊕ n) ↦ Membership.mem (γ := Set (m ⊕ n)) (Set.range Sum.inl) x) (Sum.inl a) sorry)) :
      m ⊕ n) :
    m ⊕ n)
  ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a) : m ⊕ n)
Tactic: rw [ofInjective_apply, Subtype.coe_mk, Subtype.coe_mk]
-- 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 : m
⊢ Eq (α := m ⊕ n)
    ((↑((σ₁' : (a : (↑(Set.range Sum.inl) : Type (max u_2 u_1))) → (↑(Set.range Sum.inl) : Type (max u_2 u_1)))
            (Subtype.mk (p := fun (x : m ⊕ n) ↦ Membership.mem (γ := Set (m ⊕ n)) (Set.range Sum.inl) x) (Sum.inl a)
              ⋯)) :
        m ⊕ n) :
      m ⊕ n)
    ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a) : m ⊕ n)
have h₁ : Eq (α := m ⊕ n)
  ((↑((σ₁' : (a : { x : m ⊕ n // ∃ (y : m), Sum.inl y = x }) → { x : m ⊕ n // ∃ (y : m), Sum.inl y = x })
          (Subtype.mk (p := fun (x : m ⊕ n) ↦ ∃ (y : m), Sum.inl y = x) (Sum.inl a) sorry)) :
      m ⊕ n) :
    m ⊕ n)
  ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a) : m ⊕ n)
Tactic: dsimp [Set.range]
-- 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 : m
⊢ Eq (α := m ⊕ n)
    ((↑((σ₁' : (a : { x : m ⊕ n // ∃ (y : m), Sum.inl y = x }) → { x : m ⊕ n // ∃ (y : m), Sum.inl y = x })
            (Subtype.mk (p := fun (x : m ⊕ n) ↦ ∃ (y : m), Sum.inl y = x) (Sum.inl a) ⋯)) :
        m ⊕ n) :
      m ⊕ n)
    ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a) : m ⊕ n)
have h₁ : Eq (α := m ⊕ n)
  ((↑(Subtype.mk (p := fun (x : m ⊕ n) ↦ ∃ (a : m), Sum.inl a = x)
          ((σ : (a : m ⊕ n) → m ⊕ n)
            (↑(Subtype.mk (p := fun (x : m ⊕ n) ↦ ∃ (y : m), Sum.inl y = x) (Sum.inl a) sorry) : m ⊕ n))
          sorry) :
      m ⊕ n) :
    m ⊕ n)
  ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a) : m ⊕ n)
Tactic: rw [subtypePerm_apply]
-- 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) σ₂'
b : n
⊢ Eq (α := m ⊕ n) (((σ₁, σ₂).1.sumCongr (σ₁, σ₂).2 : (a : m ⊕ n) → m ⊕ n) (Sum.inr b) : m ⊕ n)
    ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inr b) : m ⊕ n)
have h₁ : Eq (α := m ⊕ n)
  ((↑((σ₂' : (a : (↑(Set.range Sum.inr) : Type (max u_2 u_1))) → (↑(Set.range Sum.inr) : Type (max u_2 u_1)))
          (Subtype.mk (p := fun (x : m ⊕ n) ↦ Membership.mem (γ := Set (m ⊕ n)) (Set.range Sum.inr) x) (Sum.inr b) sorry)) :
      m ⊕ n) :
    m ⊕ n)
  ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inr b) : m ⊕ n)
Tactic: rw [Equiv.sumCongr_apply, Sum.map_inr, permCongr_apply, Equiv.symm_symm,
      apply_ofInjective_symm Sum.inr_injective, ofInjective_apply]
-- 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) σ₂'
b : n
⊢ Eq (α := m ⊕ n)
    ((↑((σ₂' : (a : (↑(Set.range Sum.inr) : Type (max u_2 u_1))) → (↑(Set.range Sum.inr) : Type (max u_2 u_1)))
            (Subtype.mk (p := fun (x : m ⊕ n) ↦ Membership.mem (γ := Set (m ⊕ n)) (Set.range Sum.inr) x) (Sum.inr b)
              ⋯)) :
        m ⊕ n) :
      m ⊕ n)
    ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inr b) : m ⊕ n)
have h₁ : Eq (α := m ⊕ n)
  ((↑((σ₂' : (a : { x : m ⊕ n // ∃ (y : n), Sum.inr y = x }) → { x : m ⊕ n // ∃ (y : n), Sum.inr y = x })
          (Subtype.mk (p := fun (x : m ⊕ n) ↦ ∃ (y : n), Sum.inr y = x) (Sum.inr b) sorry)) :
      m ⊕ n) :
    m ⊕ n)
  ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inr b) : m ⊕ n)
Tactic: dsimp [Set.range]
-- 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) σ₂'
b : n
⊢ Eq (α := m ⊕ n)
    ((↑((σ₂' : (a : { x : m ⊕ n // ∃ (y : n), Sum.inr y = x }) → { x : m ⊕ n // ∃ (y : n), Sum.inr y = x })
            (Subtype.mk (p := fun (x : m ⊕ n) ↦ ∃ (y : n), Sum.inr y = x) (Sum.inr b) ⋯)) :
        m ⊕ n) :
      m ⊕ n)
    ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inr b) : m ⊕ n)
have h₁ : Eq (α := m ⊕ n)
  ((↑(Subtype.mk (p := fun (x : m ⊕ n) ↦ ∃ (b : n), Sum.inr b = x)
          ((σ : (a : m ⊕ n) → m ⊕ n)
            (↑(Subtype.mk (p := fun (x : m ⊕ n) ↦ ∃ (y : n), Sum.inr y = x) (Sum.inr b) sorry) : m ⊕ n))
          sorry) :
      m ⊕ n) :
    m ⊕ n)
  ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inr b) : m ⊕ n)
Tactic: rw [subtypePerm_apply]
-- 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)
⊢ σ ∈ (sumCongrHom m n).range
have have : ∀ (x : m ⊕ n), (∃ (a : m), Sum.inl a = x) → ∃ (a : m), Eq (α := m ⊕ n) (Sum.inl a) ((σ : (a : m ⊕ n) → m ⊕ n) x)
Tactic: classical
  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⟩
  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⟩
  let σ₁' := subtypePermOfFintype σ h1
  let σ₂' := subtypePermOfFintype σ h3
  let σ₁ := permCongr (Equiv.ofInjective _ Sum.inl_injective).symm σ₁'
  let σ₂ := permCongr (Equiv.ofInjective _ Sum.inr_injective).symm σ₂'
  rw [MonoidHom.mem_range, Prod.exists]
  use σ₁, σ₂
  rw [Perm.sumCongrHom_apply]
  ext (a | b)
  · rw [Equiv.sumCongr_apply, Sum.map_inl, permCongr_apply, Equiv.symm_symm,
      apply_ofInjective_symm Sum.inl_injective]
    rw [ofInjective_apply, Subtype.coe_mk, Subtype.coe_mk]
    dsimp [Set.range]
    rw [subtypePerm_apply]
  · rw [Equiv.sumCongr_apply, Sum.map_inr, permCongr_apply, Equiv.symm_symm,
      apply_ofInjective_symm Sum.inr_injective, ofInjective_apply]
    dsimp [Set.range]
    rw [subtypePerm_apply]
-- 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)
have : ∀ (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 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)),
  σ ∈ (sumCongrHom m n).range
Tactic: classical
  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⟩
  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⟩
  let σ₁' := subtypePermOfFintype σ h1
  let σ₂' := subtypePermOfFintype σ h3
  let σ₁ := permCongr (Equiv.ofInjective _ Sum.inl_injective).symm σ₁'
  let σ₂ := permCongr (Equiv.ofInjective _ Sum.inr_injective).symm σ₂'
  rw [MonoidHom.mem_range, Prod.exists]
  use σ₁, σ₂
  rw [Perm.sumCongrHom_apply]
  ext (a | b)
  · rw [Equiv.sumCongr_apply, Sum.map_inl, permCongr_apply, Equiv.symm_symm,
      apply_ofInjective_symm Sum.inl_injective]
    rw [ofInjective_apply, Subtype.coe_mk, Subtype.coe_mk]
    dsimp [Set.range]
    rw [subtypePerm_apply]
  · rw [Equiv.sumCongr_apply, Sum.map_inr, permCongr_apply, Equiv.symm_symm,
      apply_ofInjective_symm Sum.inr_injective, ofInjective_apply]
    dsimp [Set.range]
    rw [subtypePerm_apply]
-- 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)
have : ∀ (x : m ⊕ n), (∃ (a : m), Sum.inl a = x) → ∃ (a : m), Eq (α := m ⊕ n) (Sum.inl a) ((σ : (a : m ⊕ n) → m ⊕ n) x)
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)),
    σ ∈ (sumCongrHom m n).range
have₂ : ∀ (x : m ⊕ n), (∃ (a : m), Sum.inl a = x) → ∃ (a : m), Eq (α := m ⊕ n) (Sum.inl a) ((σ : (a : m ⊕ n) → m ⊕ n) x)
have₃ 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)),
    σ ∈ (sumCongrHom m n).range
⊢ σ ∈ (sumCongrHom m n).range
have 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))
  (h3 :
    ∀ (x : m ⊕ n), (∃ (b : n), Sum.inr b = x) → ∃ (b : n), Eq (α := m ⊕ n) (Sum.inr b) ((σ : (a : m ⊕ n) → m ⊕ n) x)),
  σ ∈ (sumCongrHom m n).range
Tactic: classical
  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⟩
  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⟩
  let σ₁' := subtypePermOfFintype σ h1
  let σ₂' := subtypePermOfFintype σ h3
  let σ₁ := permCongr (Equiv.ofInjective _ Sum.inl_injective).symm σ₁'
  let σ₂ := permCongr (Equiv.ofInjective _ Sum.inr_injective).symm σ₂'
  rw [MonoidHom.mem_range, Prod.exists]
  use σ₁, σ₂
  rw [Perm.sumCongrHom_apply]
  ext (a | b)
  · rw [Equiv.sumCongr_apply, Sum.map_inl, permCongr_apply, Equiv.symm_symm,
      apply_ofInjective_symm Sum.inl_injective]
    rw [ofInjective_apply, Subtype.coe_mk, Subtype.coe_mk]
    dsimp [Set.range]
    rw [subtypePerm_apply]
  · rw [Equiv.sumCongr_apply, Sum.map_inr, permCongr_apply, Equiv.symm_symm,
      apply_ofInjective_symm Sum.inr_injective, ofInjective_apply]
    dsimp [Set.range]
    rw [subtypePerm_apply]
-- 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)
have : ∀ (x : m ⊕ n), (∃ (a : m), Sum.inl a = x) → ∃ (a : m), Eq (α := m ⊕ n) (Sum.inl a) ((σ : (a : m ⊕ n) → m ⊕ n) x)
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)),
    σ ∈ (sumCongrHom m n).range
have₂ : ∀ (x : m ⊕ n), (∃ (a : m), Sum.inl a = x) → ∃ (a : m), Eq (α := m ⊕ n) (Sum.inl a) ((σ : (a : m ⊕ n) → m ⊕ n) x)
have₃ 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)),
    σ ∈ (sumCongrHom m n).range
have₅ have₆ have₇ have₈ 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))
    (h3 :
      ∀ (x : m ⊕ n), (∃ (b : n), Sum.inr b = x) → ∃ (b : n), Eq (α := m ⊕ n) (Sum.inr b) ((σ : (a : m ⊕ n) → m ⊕ n) x)),
    σ ∈ (sumCongrHom m n).range
⊢ σ ∈ (sumCongrHom m n).range
have 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))
  (h3 :
    ∀ (x : m ⊕ n), (∃ (b : n), Sum.inr b = x) → ∃ (b : n), Eq (α := m ⊕ n) (Sum.inr b) ((σ : (a : m ⊕ n) → m ⊕ n) x)),
  ∃ (a : Perm m) (b : Perm n), (sumCongrHom m n : (a : Perm m × Perm n) → Perm (m ⊕ n)) (a, b) = σ
Tactic: classical
  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⟩
  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⟩
  let σ₁' := subtypePermOfFintype σ h1
  let σ₂' := subtypePermOfFintype σ h3
  let σ₁ := permCongr (Equiv.ofInjective _ Sum.inl_injective).symm σ₁'
  let σ₂ := permCongr (Equiv.ofInjective _ Sum.inr_injective).symm σ₂'
  rw [MonoidHom.mem_range, Prod.exists]
  use σ₁, σ₂
  rw [Perm.sumCongrHom_apply]
  ext (a | b)
  · rw [Equiv.sumCongr_apply, Sum.map_inl, permCongr_apply, Equiv.symm_symm,
      apply_ofInjective_symm Sum.inl_injective]
    rw [ofInjective_apply, Subtype.coe_mk, Subtype.coe_mk]
    dsimp [Set.range]
    rw [subtypePerm_apply]
  · rw [Equiv.sumCongr_apply, Sum.map_inr, permCongr_apply, Equiv.symm_symm,
      apply_ofInjective_symm Sum.inr_injective, ofInjective_apply]
    dsimp [Set.range]
    rw [subtypePerm_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
σ τ : Perm α
hστ : σ.Disjoint τ
n : ℕ
⊢ (σ * τ) ^ n = 1 ↔ σ ^ n = 1 ∧ τ ^ n = 1
have rw : σ ^ n * τ ^ n = 1 ↔ σ ^ n = 1 ∧ τ ^ n = 1
Tactic: rw [hστ.commute.mul_pow, Disjoint.mul_eq_one_iff (hστ.pow_disjoint_pow n n)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
σ τ : Perm α
hστ : σ.Disjoint τ
n : ℕ
rw : σ ^ n * τ ^ n = 1 ↔ σ ^ n = 1 ∧ τ ^ n = 1
⊢ (σ * τ) ^ n = 1 ↔ σ ^ n = 1 ∧ τ ^ n = 1
have rw₁ : σ ^ n = 1 ∧ τ ^ n = 1 ↔ σ ^ n = 1 ∧ τ ^ n = 1
Tactic: rw [hστ.commute.mul_pow, Disjoint.mul_eq_one_iff (hστ.pow_disjoint_pow n n)]
-- 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 : β
⊢ (σ.extendDomain (p := p) f : (a : β) → β) b = b ∨ (τ.extendDomain (p := p) f : (a : β) → β) b = b
have pos : ∀ (pb : p b), (σ.extendDomain (p := p) f : (a : β) → β) b = b ∨ (τ.extendDomain (p := p) f : (a : β) → β) b = b
Tactic: by_cases pb : p b
-- 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 : β
pos : ∀ (pb : p b), (σ.extendDomain (p := p) f : (a : β) → β) b = b ∨ (τ.extendDomain (p := p) f : (a : β) → β) b = b
⊢ (σ.extendDomain (p := p) f : (a : β) → β) b = b ∨ (τ.extendDomain (p := p) f : (a : β) → β) b = b
have neg : ∀ (pb : ¬p b), (σ.extendDomain (p := p) f : (a : β) → β) b = b ∨ (τ.extendDomain (p := p) f : (a : β) → β) b = b
Tactic: by_cases pb : p b