case intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝ : Fintype m
⊢ σ ∈ MonoidHom.range (sumCongrHom m n)
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
⊢ σ ∈ MonoidHom.range (sumCongrHom m n)
cases nonempty_fintype m
case intro.intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
⊢ σ ∈ MonoidHom.range (sumCongrHom m n)
case intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝ : Fintype m
⊢ σ ∈ MonoidHom.range (sumCongrHom m n)
cases nonempty_fintype n
case intro.intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
⊢ σ ∈ MonoidHom.range (sumCongrHom m n)
case intro.intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
⊢ σ ∈ MonoidHom.range (sumCongrHom m n)
have h1 : ∀ x : Sum m n, (∃ a : m, Sum.inl a = x) → ∃ a : m, Sum.inl a = σ x := by
  rintro x ⟨a, ha⟩
  apply h
  rw [← ha]
  exact ⟨a, rfl⟩
case intro.intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = ↑σ x
⊢ σ ∈ MonoidHom.range (sumCongrHom m n)
case intro.intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
⊢ σ ∈ MonoidHom.range (sumCongrHom m n)
have h3 : ∀ x : Sum m n, (∃ b : n, Sum.inr b = x) → ∃ b : n, Sum.inr b = σ x := by
  rintro x ⟨b, hb⟩
  apply (perm_mapsTo_inl_iff_mapsTo_inr σ).mp h
  rw [← hb]
  exact ⟨b, rfl⟩
case intro.intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = ↑σ x
σ₁' : Perm { x // ∃ a, Sum.inl a = x } := subtypePermOfFintype σ h1
⊢ σ ∈ MonoidHom.range (sumCongrHom m n)
case intro.intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = ↑σ x
⊢ σ ∈ MonoidHom.range (sumCongrHom m n)
let σ₁' := subtypePermOfFintype σ h1
case intro.intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = ↑σ x
σ₁' : Perm { x // ∃ a, Sum.inl a = x } := subtypePermOfFintype σ h1
σ₂' : Perm { x // ∃ b, Sum.inr b = x } := subtypePermOfFintype σ h3
⊢ σ ∈ MonoidHom.range (sumCongrHom m n)
case intro.intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = ↑σ x
σ₁' : Perm { x // ∃ a, Sum.inl a = x } := subtypePermOfFintype σ h1
⊢ σ ∈ MonoidHom.range (sumCongrHom m n)
let σ₂' := subtypePermOfFintype σ h3
case intro.intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = ↑σ x
σ₁' : Perm { x // ∃ a, Sum.inl a = x } := subtypePermOfFintype σ h1
σ₂' : Perm { x // ∃ b, Sum.inr b = x } := subtypePermOfFintype σ h3
σ₁ : (fun x => Perm m) σ₁' := ↑(permCongr (ofInjective Sum.inl (_ : Injective Sum.inl)).symm) σ₁'
⊢ σ ∈ MonoidHom.range (sumCongrHom m n)
case intro.intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = ↑σ x
σ₁' : Perm { x // ∃ a, Sum.inl a = x } := subtypePermOfFintype σ h1
σ₂' : Perm { x // ∃ b, Sum.inr b = x } := subtypePermOfFintype σ h3
⊢ σ ∈ MonoidHom.range (sumCongrHom m n)
let σ₁ := permCongr (Equiv.ofInjective _ Sum.inl_injective).symm σ₁'
case intro.intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = ↑σ x
σ₁' : Perm { x // ∃ a, Sum.inl a = x } := subtypePermOfFintype σ h1
σ₂' : Perm { x // ∃ b, Sum.inr b = x } := subtypePermOfFintype σ h3
σ₁ : (fun x => Perm m) σ₁' := ↑(permCongr (ofInjective Sum.inl (_ : Injective Sum.inl)).symm) σ₁'
σ₂ : (fun x => Perm n) σ₂' := ↑(permCongr (ofInjective Sum.inr (_ : Injective Sum.inr)).symm) σ₂'
⊢ σ ∈ MonoidHom.range (sumCongrHom m n)
case intro.intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = ↑σ x
σ₁' : Perm { x // ∃ a, Sum.inl a = x } := subtypePermOfFintype σ h1
σ₂' : Perm { x // ∃ b, Sum.inr b = x } := subtypePermOfFintype σ h3
σ₁ : (fun x => Perm m) σ₁' := ↑(permCongr (ofInjective Sum.inl (_ : Injective Sum.inl)).symm) σ₁'
⊢ σ ∈ MonoidHom.range (sumCongrHom m n)
let σ₂ := permCongr (Equiv.ofInjective _ Sum.inr_injective).symm σ₂'
case intro.intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = ↑σ x
σ₁' : Perm { x // ∃ a, Sum.inl a = x } := subtypePermOfFintype σ h1
σ₂' : Perm { x // ∃ b, Sum.inr b = x } := subtypePermOfFintype σ h3
σ₁ : (fun x => Perm m) σ₁' := ↑(permCongr (ofInjective Sum.inl (_ : Injective Sum.inl)).symm) σ₁'
σ₂ : (fun x => Perm n) σ₂' := ↑(permCongr (ofInjective Sum.inr (_ : Injective Sum.inr)).symm) σ₂'
⊢ ∃ a b, ↑(sumCongrHom m n) (a, b) = σ
case intro.intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = ↑σ x
σ₁' : Perm { x // ∃ a, Sum.inl a = x } := subtypePermOfFintype σ h1
σ₂' : Perm { x // ∃ b, Sum.inr b = x } := subtypePermOfFintype σ h3
σ₁ : (fun x => Perm m) σ₁' := ↑(permCongr (ofInjective Sum.inl (_ : Injective Sum.inl)).symm) σ₁'
σ₂ : (fun x => Perm n) σ₂' := ↑(permCongr (ofInjective Sum.inr (_ : Injective Sum.inr)).symm) σ₂'
⊢ σ ∈ MonoidHom.range (sumCongrHom m n)
rw [MonoidHom.mem_range, Prod.exists]
case intro.intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = ↑σ x
σ₁' : Perm { x // ∃ a, Sum.inl a = x } := subtypePermOfFintype σ h1
σ₂' : Perm { x // ∃ b, Sum.inr b = x } := subtypePermOfFintype σ h3
σ₁ : (fun x => Perm m) σ₁' := ↑(permCongr (ofInjective Sum.inl (_ : Injective Sum.inl)).symm) σ₁'
σ₂ : (fun x => Perm n) σ₂' := ↑(permCongr (ofInjective Sum.inr (_ : Injective Sum.inr)).symm) σ₂'
⊢ ↑(sumCongrHom m n) (σ₁, σ₂) = σ
case intro.intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = ↑σ x
σ₁' : Perm { x // ∃ a, Sum.inl a = x } := subtypePermOfFintype σ h1
σ₂' : Perm { x // ∃ b, Sum.inr b = x } := subtypePermOfFintype σ h3
σ₁ : (fun x => Perm m) σ₁' := ↑(permCongr (ofInjective Sum.inl (_ : Injective Sum.inl)).symm) σ₁'
σ₂ : (fun x => Perm n) σ₂' := ↑(permCongr (ofInjective Sum.inr (_ : Injective Sum.inr)).symm) σ₂'
⊢ ∃ a b, ↑(sumCongrHom m n) (a, b) = σ
use σ₁, σ₂
case intro.intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = ↑σ x
σ₁' : Perm { x // ∃ a, Sum.inl a = x } := subtypePermOfFintype σ h1
σ₂' : Perm { x // ∃ b, Sum.inr b = x } := subtypePermOfFintype σ h3
σ₁ : (fun x => Perm m) σ₁' := ↑(permCongr (ofInjective Sum.inl (_ : Injective Sum.inl)).symm) σ₁'
σ₂ : (fun x => Perm n) σ₂' := ↑(permCongr (ofInjective Sum.inr (_ : Injective Sum.inr)).symm) σ₂'
⊢ sumCongr (σ₁, σ₂).fst (σ₁, σ₂).snd = σ
case intro.intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = ↑σ x
σ₁' : Perm { x // ∃ a, Sum.inl a = x } := subtypePermOfFintype σ h1
σ₂' : Perm { x // ∃ b, Sum.inr b = x } := subtypePermOfFintype σ h3
σ₁ : (fun x => Perm m) σ₁' := ↑(permCongr (ofInjective Sum.inl (_ : Injective Sum.inl)).symm) σ₁'
σ₂ : (fun x => Perm n) σ₂' := ↑(permCongr (ofInjective Sum.inr (_ : Injective Sum.inr)).symm) σ₂'
⊢ ↑(sumCongrHom m n) (σ₁, σ₂) = σ
rw [Perm.sumCongrHom_apply]
case intro.intro.H
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = ↑σ x
σ₁' : Perm { x // ∃ a, Sum.inl a = x } := subtypePermOfFintype σ h1
σ₂' : Perm { x // ∃ b, Sum.inr b = x } := subtypePermOfFintype σ h3
σ₁ : (fun x => Perm m) σ₁' := ↑(permCongr (ofInjective Sum.inl (_ : Injective Sum.inl)).symm) σ₁'
σ₂ : (fun x => Perm n) σ₂' := ↑(permCongr (ofInjective Sum.inr (_ : Injective Sum.inr)).symm) σ₂'
x : m ⊕ n
⊢ ↑(sumCongr (σ₁, σ₂).fst (σ₁, σ₂).snd) x = ↑σ x
case intro.intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = ↑σ x
σ₁' : Perm { x // ∃ a, Sum.inl a = x } := subtypePermOfFintype σ h1
σ₂' : Perm { x // ∃ b, Sum.inr b = x } := subtypePermOfFintype σ h3
σ₁ : (fun x => Perm m) σ₁' := ↑(permCongr (ofInjective Sum.inl (_ : Injective Sum.inl)).symm) σ₁'
σ₂ : (fun x => Perm n) σ₂' := ↑(permCongr (ofInjective Sum.inr (_ : Injective Sum.inr)).symm) σ₂'
⊢ sumCongr (σ₁, σ₂).fst (σ₁, σ₂).snd = σ
ext x
case intro.intro.H.inl
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = ↑σ x
σ₁' : Perm { x // ∃ a, Sum.inl a = x } := subtypePermOfFintype σ h1
σ₂' : Perm { x // ∃ b, Sum.inr b = x } := subtypePermOfFintype σ h3
σ₁ : (fun x => Perm m) σ₁' := ↑(permCongr (ofInjective Sum.inl (_ : Injective Sum.inl)).symm) σ₁'
σ₂ : (fun x => Perm n) σ₂' := ↑(permCongr (ofInjective Sum.inr (_ : Injective Sum.inr)).symm) σ₂'
a : m
⊢ ↑(sumCongr (σ₁, σ₂).fst (σ₁, σ₂).snd) (Sum.inl a) = ↑σ (Sum.inl a)

case intro.intro.H.inr
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = ↑σ x
σ₁' : Perm { x // ∃ a, Sum.inl a = x } := subtypePermOfFintype σ h1
σ₂' : Perm { x // ∃ b, Sum.inr b = x } := subtypePermOfFintype σ h3
σ₁ : (fun x => Perm m) σ₁' := ↑(permCongr (ofInjective Sum.inl (_ : Injective Sum.inl)).symm) σ₁'
σ₂ : (fun x => Perm n) σ₂' := ↑(permCongr (ofInjective Sum.inr (_ : Injective Sum.inr)).symm) σ₂'
b : n
⊢ ↑(sumCongr (σ₁, σ₂).fst (σ₁, σ₂).snd) (Sum.inr b) = ↑σ (Sum.inr b)
case intro.intro.H
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = ↑σ x
σ₁' : Perm { x // ∃ a, Sum.inl a = x } := subtypePermOfFintype σ h1
σ₂' : Perm { x // ∃ b, Sum.inr b = x } := subtypePermOfFintype σ h3
σ₁ : (fun x => Perm m) σ₁' := ↑(permCongr (ofInjective Sum.inl (_ : Injective Sum.inl)).symm) σ₁'
σ₂ : (fun x => Perm n) σ₂' := ↑(permCongr (ofInjective Sum.inr (_ : Injective Sum.inr)).symm) σ₂'
x : m ⊕ n
⊢ ↑(sumCongr (σ₁, σ₂).fst (σ₁, σ₂).snd) x = ↑σ x
cases' x with a b
case intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
x : m ⊕ n
a : m
ha : Sum.inl a = x
⊢ ∃ a, Sum.inl a = ↑σ x
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
⊢ ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
rintro x ⟨a, ha⟩
case intro.a
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
x : m ⊕ n
a : m
ha : Sum.inl a = x
⊢ x ∈ Set.range Sum.inl
case intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
x : m ⊕ n
a : m
ha : Sum.inl a = x
⊢ ∃ a, Sum.inl a = ↑σ x
apply h
case intro.a
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
x : m ⊕ n
a : m
ha : Sum.inl a = x
⊢ Sum.inl a ∈ Set.range Sum.inl
case intro.a
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
x : m ⊕ n
a : m
ha : Sum.inl a = x
⊢ x ∈ Set.range Sum.inl
rw [← ha]
no goals
case intro.a
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
x : m ⊕ n
a : m
ha : Sum.inl a = x
⊢ Sum.inl a ∈ Set.range Sum.inl
exact ⟨a, rfl⟩
case intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
x : m ⊕ n
b : n
hb : Sum.inr b = x
⊢ ∃ b, Sum.inr b = ↑σ x
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
⊢ ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = ↑σ x
rintro x ⟨b, hb⟩
case intro.a
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
x : m ⊕ n
b : n
hb : Sum.inr b = x
⊢ x ∈ Set.range Sum.inr
case intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
x : m ⊕ n
b : n
hb : Sum.inr b = x
⊢ ∃ b, Sum.inr b = ↑σ x
apply (perm_mapsTo_inl_iff_mapsTo_inr σ).mp h
case intro.a
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
x : m ⊕ n
b : n
hb : Sum.inr b = x
⊢ Sum.inr b ∈ Set.range Sum.inr
case intro.a
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
x : m ⊕ n
b : n
hb : Sum.inr b = x
⊢ x ∈ Set.range Sum.inr
rw [← hb]
no goals
case intro.a
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
x : m ⊕ n
b : n
hb : Sum.inr b = x
⊢ Sum.inr b ∈ Set.range Sum.inr
exact ⟨b, rfl⟩
case intro.intro.H.inl
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = ↑σ x
σ₁' : Perm { x // ∃ a, Sum.inl a = x } := subtypePermOfFintype σ h1
σ₂' : Perm { x // ∃ b, Sum.inr b = x } := subtypePermOfFintype σ h3
σ₁ : (fun x => Perm m) σ₁' := ↑(permCongr (ofInjective Sum.inl (_ : Injective Sum.inl)).symm) σ₁'
σ₂ : (fun x => Perm n) σ₂' := ↑(permCongr (ofInjective Sum.inr (_ : Injective Sum.inr)).symm) σ₂'
a : m
⊢ ↑(↑σ₁' (↑(ofInjective Sum.inl (_ : Injective Sum.inl)) a)) = ↑σ (Sum.inl a)
case intro.intro.H.inl
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = ↑σ x
σ₁' : Perm { x // ∃ a, Sum.inl a = x } := subtypePermOfFintype σ h1
σ₂' : Perm { x // ∃ b, Sum.inr b = x } := subtypePermOfFintype σ h3
σ₁ : (fun x => Perm m) σ₁' := ↑(permCongr (ofInjective Sum.inl (_ : Injective Sum.inl)).symm) σ₁'
σ₂ : (fun x => Perm n) σ₂' := ↑(permCongr (ofInjective Sum.inr (_ : Injective Sum.inr)).symm) σ₂'
a : m
⊢ ↑(sumCongr (σ₁, σ₂).fst (σ₁, σ₂).snd) (Sum.inl a) = ↑σ (Sum.inl a)
rw [Equiv.sumCongr_apply, Sum.map_inl, permCongr_apply, Equiv.symm_symm,
  apply_ofInjective_symm Sum.inl_injective]
no goals
case intro.intro.H.inl
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = ↑σ x
σ₁' : Perm { x // ∃ a, Sum.inl a = x } := subtypePermOfFintype σ h1
σ₂' : Perm { x // ∃ b, Sum.inr b = x } := subtypePermOfFintype σ h3
σ₁ : (fun x => Perm m) σ₁' := ↑(permCongr (ofInjective Sum.inl (_ : Injective Sum.inl)).symm) σ₁'
σ₂ : (fun x => Perm n) σ₂' := ↑(permCongr (ofInjective Sum.inr (_ : Injective Sum.inr)).symm) σ₂'
a : m
⊢ ↑(↑σ₁' (↑(ofInjective Sum.inl (_ : Injective Sum.inl)) a)) = ↑σ (Sum.inl a)
rw [ofInjective_apply, Subtype.coe_mk, Subtype.coe_mk, subtypePerm_apply]
case intro.intro.H.inr
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = ↑σ x
σ₁' : Perm { x // ∃ a, Sum.inl a = x } := subtypePermOfFintype σ h1
σ₂' : Perm { x // ∃ b, Sum.inr b = x } := subtypePermOfFintype σ h3
σ₁ : (fun x => Perm m) σ₁' := ↑(permCongr (ofInjective Sum.inl (_ : Injective Sum.inl)).symm) σ₁'
σ₂ : (fun x => Perm n) σ₂' := ↑(permCongr (ofInjective Sum.inr (_ : Injective Sum.inr)).symm) σ₂'
b : n
⊢ ↑(↑σ₂' (↑(ofInjective Sum.inr (_ : Injective Sum.inr)) b)) = ↑σ (Sum.inr b)
case intro.intro.H.inr
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = ↑σ x
σ₁' : Perm { x // ∃ a, Sum.inl a = x } := subtypePermOfFintype σ h1
σ₂' : Perm { x // ∃ b, Sum.inr b = x } := subtypePermOfFintype σ h3
σ₁ : (fun x => Perm m) σ₁' := ↑(permCongr (ofInjective Sum.inl (_ : Injective Sum.inl)).symm) σ₁'
σ₂ : (fun x => Perm n) σ₂' := ↑(permCongr (ofInjective Sum.inr (_ : Injective Sum.inr)).symm) σ₂'
b : n
⊢ ↑(sumCongr (σ₁, σ₂).fst (σ₁, σ₂).snd) (Sum.inr b) = ↑σ (Sum.inr b)
rw [Equiv.sumCongr_apply, Sum.map_inr, permCongr_apply, Equiv.symm_symm,
  apply_ofInjective_symm Sum.inr_injective]
case intro.intro.H.inr
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = ↑σ x
σ₁' : Perm { x // ∃ a, Sum.inl a = x } := subtypePermOfFintype σ h1
σ₂' : Perm { x // ∃ b, Sum.inr b = x } := subtypePermOfFintype σ h3
σ₁ : (fun x => Perm m) σ₁' := ↑(permCongr (ofInjective Sum.inl (_ : Injective Sum.inl)).symm) σ₁'
σ₂ : (fun x => Perm n) σ₂' := ↑(permCongr (ofInjective Sum.inr (_ : Injective Sum.inr)).symm) σ₂'
b : n
⊢ ↑{ val := ↑σ ↑(↑(ofInjective Sum.inr (_ : Injective Sum.inr)) b),
        property := (_ : (fun x => ∃ b, Sum.inr b = x) (↑σ ↑(↑(ofInjective Sum.inr (_ : Injective Sum.inr)) b))) } =
    ↑σ (Sum.inr b)
case intro.intro.H.inr
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = ↑σ x
σ₁' : Perm { x // ∃ a, Sum.inl a = x } := subtypePermOfFintype σ h1
σ₂' : Perm { x // ∃ b, Sum.inr b = x } := subtypePermOfFintype σ h3
σ₁ : (fun x => Perm m) σ₁' := ↑(permCongr (ofInjective Sum.inl (_ : Injective Sum.inl)).symm) σ₁'
σ₂ : (fun x => Perm n) σ₂' := ↑(permCongr (ofInjective Sum.inr (_ : Injective Sum.inr)).symm) σ₂'
b : n
⊢ ↑(↑σ₂' (↑(ofInjective Sum.inr (_ : Injective Sum.inr)) b)) = ↑σ (Sum.inr b)
erw [subtypePerm_apply]
no goals
case intro.intro.H.inr
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = ↑σ x
σ₁' : Perm { x // ∃ a, Sum.inl a = x } := subtypePermOfFintype σ h1
σ₂' : Perm { x // ∃ b, Sum.inr b = x } := subtypePermOfFintype σ h3
σ₁ : (fun x => Perm m) σ₁' := ↑(permCongr (ofInjective Sum.inl (_ : Injective Sum.inl)).symm) σ₁'
σ₂ : (fun x => Perm n) σ₂' := ↑(permCongr (ofInjective Sum.inr (_ : Injective Sum.inr)).symm) σ₂'
b : n
⊢ ↑{ val := ↑σ ↑(↑(ofInjective Sum.inr (_ : Injective Sum.inr)) b),
        property := (_ : (fun x => ∃ b, Sum.inr b = x) (↑σ ↑(↑(ofInjective Sum.inr (_ : Injective Sum.inr)) b))) } =
    ↑σ (Sum.inr b)
rw [ofInjective_apply, Subtype.coe_mk, Subtype.coe_mk]