case intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝ : Fintype m
⊢ Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl) ↔ Set.MapsTo (↑σ) (Set.range Sum.inr) (Set.range Sum.inr)
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
⊢ Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl) ↔ Set.MapsTo (↑σ) (Set.range Sum.inr) (Set.range Sum.inr)
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)
val✝¹ : Fintype m
val✝ : Fintype n
⊢ Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl) ↔ Set.MapsTo (↑σ) (Set.range Sum.inr) (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)
val✝ : Fintype m
⊢ Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl) ↔ Set.MapsTo (↑σ) (Set.range Sum.inr) (Set.range Sum.inr)
cases nonempty_fintype n
case intro.intro.mp.inl
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ⁻¹) (Set.range Sum.inl) (Set.range Sum.inl)
x : m ⊕ n
l : m
hx : ↑σ x = Sum.inl l
⊢ x ∈ Set.range Sum.inr → Sum.inl l ∈ Set.range Sum.inr

case intro.intro.mp.inr
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ⁻¹) (Set.range Sum.inl) (Set.range Sum.inl)
x : m ⊕ n
r : n
hx : ↑σ x = Sum.inr r
⊢ x ∈ Set.range Sum.inr → Sum.inr r ∈ Set.range Sum.inr

case intro.intro.mpr.inl
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ⁻¹) (Set.range Sum.inr) (Set.range Sum.inr)
x : m ⊕ n
l : m
hx : ↑σ x = Sum.inl l
⊢ x ∈ Set.range Sum.inl → Sum.inl l ∈ Set.range Sum.inl

case intro.intro.mpr.inr
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ⁻¹) (Set.range Sum.inr) (Set.range Sum.inr)
x : m ⊕ n
r : n
hx : ↑σ x = Sum.inr r
⊢ x ∈ Set.range Sum.inl → Sum.inr r ∈ Set.range Sum.inl
case intro.intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
⊢ Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl) ↔ Set.MapsTo (↑σ) (Set.range Sum.inr) (Set.range Sum.inr)
constructor <;>
  ( intro h
    classical
      rw [← perm_inv_mapsTo_iff_mapsTo] at h
      intro x
      cases' hx : σ x with l r)
case intro.intro.mpr
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ) (Set.range Sum.inr) (Set.range Sum.inr)
⊢ Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
case intro.intro.mpr
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
⊢ Set.MapsTo (↑σ) (Set.range Sum.inr) (Set.range Sum.inr) → Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
intro h
case intro.intro.mpr.inl
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ⁻¹) (Set.range Sum.inr) (Set.range Sum.inr)
x : m ⊕ n
l : m
hx : ↑σ x = Sum.inl l
⊢ x ∈ Set.range Sum.inl → Sum.inl l ∈ Set.range Sum.inl

case intro.intro.mpr.inr
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ⁻¹) (Set.range Sum.inr) (Set.range Sum.inr)
x : m ⊕ n
r : n
hx : ↑σ x = Sum.inr r
⊢ x ∈ Set.range Sum.inl → Sum.inr r ∈ Set.range Sum.inl
case intro.intro.mpr
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ) (Set.range Sum.inr) (Set.range Sum.inr)
⊢ Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
classical
  rw [← perm_inv_mapsTo_iff_mapsTo] at h
  intro x
  cases' hx : σ x with l r
case intro.intro.mpr
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ⁻¹) (Set.range Sum.inr) (Set.range Sum.inr)
⊢ Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
case intro.intro.mpr
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ) (Set.range Sum.inr) (Set.range Sum.inr)
⊢ Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
rw [← perm_inv_mapsTo_iff_mapsTo] at h
case intro.intro.mpr
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ⁻¹) (Set.range Sum.inr) (Set.range Sum.inr)
x : m ⊕ n
⊢ x ∈ Set.range Sum.inl → ↑σ x ∈ Set.range Sum.inl
case intro.intro.mpr
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ⁻¹) (Set.range Sum.inr) (Set.range Sum.inr)
⊢ Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
intro x
case intro.intro.mpr.inl
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ⁻¹) (Set.range Sum.inr) (Set.range Sum.inr)
x : m ⊕ n
l : m
hx : ↑σ x = Sum.inl l
⊢ x ∈ Set.range Sum.inl → Sum.inl l ∈ Set.range Sum.inl

case intro.intro.mpr.inr
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ⁻¹) (Set.range Sum.inr) (Set.range Sum.inr)
x : m ⊕ n
r : n
hx : ↑σ x = Sum.inr r
⊢ x ∈ Set.range Sum.inl → Sum.inr r ∈ Set.range Sum.inl
case intro.intro.mpr
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ⁻¹) (Set.range Sum.inr) (Set.range Sum.inr)
x : m ⊕ n
⊢ x ∈ Set.range Sum.inl → ↑σ x ∈ Set.range Sum.inl
cases' hx : σ x with l r
case intro.intro.mp.inl.intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ⁻¹) (Set.range Sum.inl) (Set.range Sum.inl)
l : m
a : n
hx : ↑σ (Sum.inr a) = Sum.inl l
⊢ Sum.inl l ∈ Set.range Sum.inr
case intro.intro.mp.inl
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ⁻¹) (Set.range Sum.inl) (Set.range Sum.inl)
x : m ⊕ n
l : m
hx : ↑σ x = Sum.inl l
⊢ x ∈ Set.range Sum.inr → Sum.inl l ∈ Set.range Sum.inr
rintro ⟨a, rfl⟩
case intro.intro.mp.inl.intro.intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ⁻¹) (Set.range Sum.inl) (Set.range Sum.inl)
l : m
a : n
hx : ↑σ (Sum.inr a) = Sum.inl l
y : m
hy : Sum.inl y = ↑σ⁻¹ (Sum.inl l)
⊢ Sum.inl l ∈ Set.range Sum.inr
case intro.intro.mp.inl.intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ⁻¹) (Set.range Sum.inl) (Set.range Sum.inl)
l : m
a : n
hx : ↑σ (Sum.inr a) = Sum.inl l
⊢ Sum.inl l ∈ Set.range Sum.inr
obtain ⟨y, hy⟩ := h ⟨l, rfl⟩
case intro.intro.mp.inl.intro.intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ⁻¹) (Set.range Sum.inl) (Set.range Sum.inl)
l : m
a : n
hx : ↑σ (Sum.inr a) = Sum.inl l
y : m
hy : Sum.inl y = Sum.inr a
⊢ Sum.inl l ∈ Set.range Sum.inr
case intro.intro.mp.inl.intro.intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ⁻¹) (Set.range Sum.inl) (Set.range Sum.inl)
l : m
a : n
hx : ↑σ (Sum.inr a) = Sum.inl l
y : m
hy : Sum.inl y = ↑σ⁻¹ (Sum.inl l)
⊢ Sum.inl l ∈ Set.range Sum.inr
rw [← hx, σ.inv_apply_self] at hy
no goals
case intro.intro.mp.inl.intro.intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ⁻¹) (Set.range Sum.inl) (Set.range Sum.inl)
l : m
a : n
hx : ↑σ (Sum.inr a) = Sum.inl l
y : m
hy : Sum.inl y = Sum.inr a
⊢ Sum.inl l ∈ Set.range Sum.inr
exact absurd hy Sum.inl_ne_inr
case intro.intro.mp.inr
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ⁻¹) (Set.range Sum.inl) (Set.range Sum.inl)
x : m ⊕ n
r : n
hx : ↑σ x = Sum.inr r
a✝ : x ∈ Set.range Sum.inr
⊢ Sum.inr r ∈ Set.range Sum.inr
case intro.intro.mp.inr
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ⁻¹) (Set.range Sum.inl) (Set.range Sum.inl)
x : m ⊕ n
r : n
hx : ↑σ x = Sum.inr r
⊢ x ∈ Set.range Sum.inr → Sum.inr r ∈ Set.range Sum.inr
rintro _
no goals
case intro.intro.mp.inr
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ⁻¹) (Set.range Sum.inl) (Set.range Sum.inl)
x : m ⊕ n
r : n
hx : ↑σ x = Sum.inr r
a✝ : x ∈ Set.range Sum.inr
⊢ Sum.inr r ∈ Set.range Sum.inr
exact ⟨r, rfl⟩
case intro.intro.mpr.inl
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ⁻¹) (Set.range Sum.inr) (Set.range Sum.inr)
x : m ⊕ n
l : m
hx : ↑σ x = Sum.inl l
a✝ : x ∈ Set.range Sum.inl
⊢ Sum.inl l ∈ Set.range Sum.inl
case intro.intro.mpr.inl
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ⁻¹) (Set.range Sum.inr) (Set.range Sum.inr)
x : m ⊕ n
l : m
hx : ↑σ x = Sum.inl l
⊢ x ∈ Set.range Sum.inl → Sum.inl l ∈ Set.range Sum.inl
rintro _
no goals
case intro.intro.mpr.inl
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ⁻¹) (Set.range Sum.inr) (Set.range Sum.inr)
x : m ⊕ n
l : m
hx : ↑σ x = Sum.inl l
a✝ : x ∈ Set.range Sum.inl
⊢ Sum.inl l ∈ Set.range Sum.inl
exact ⟨l, rfl⟩
case intro.intro.mpr.inr.intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ⁻¹) (Set.range Sum.inr) (Set.range Sum.inr)
r : n
a : m
hx : ↑σ (Sum.inl a) = Sum.inr r
⊢ Sum.inr r ∈ Set.range Sum.inl
case intro.intro.mpr.inr
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ⁻¹) (Set.range Sum.inr) (Set.range Sum.inr)
x : m ⊕ n
r : n
hx : ↑σ x = Sum.inr r
⊢ x ∈ Set.range Sum.inl → Sum.inr r ∈ Set.range Sum.inl
rintro ⟨a, rfl⟩
case intro.intro.mpr.inr.intro.intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ⁻¹) (Set.range Sum.inr) (Set.range Sum.inr)
r : n
a : m
hx : ↑σ (Sum.inl a) = Sum.inr r
y : n
hy : Sum.inr y = ↑σ⁻¹ (Sum.inr r)
⊢ Sum.inr r ∈ Set.range Sum.inl
case intro.intro.mpr.inr.intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ⁻¹) (Set.range Sum.inr) (Set.range Sum.inr)
r : n
a : m
hx : ↑σ (Sum.inl a) = Sum.inr r
⊢ Sum.inr r ∈ Set.range Sum.inl
obtain ⟨y, hy⟩ := h ⟨r, rfl⟩
case intro.intro.mpr.inr.intro.intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ⁻¹) (Set.range Sum.inr) (Set.range Sum.inr)
r : n
a : m
hx : ↑σ (Sum.inl a) = Sum.inr r
y : n
hy : Sum.inr y = Sum.inl a
⊢ Sum.inr r ∈ Set.range Sum.inl
case intro.intro.mpr.inr.intro.intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ⁻¹) (Set.range Sum.inr) (Set.range Sum.inr)
r : n
a : m
hx : ↑σ (Sum.inl a) = Sum.inr r
y : n
hy : Sum.inr y = ↑σ⁻¹ (Sum.inr r)
⊢ Sum.inr r ∈ Set.range Sum.inl
rw [← hx, σ.inv_apply_self] at hy
no goals
case intro.intro.mpr.inr.intro.intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ⁻¹) (Set.range Sum.inr) (Set.range Sum.inr)
r : n
a : m
hx : ↑σ (Sum.inl a) = Sum.inr r
y : n
hy : Sum.inr y = Sum.inl a
⊢ Sum.inr r ∈ Set.range Sum.inl
exact absurd hy Sum.inr_ne_inl