-- Mathlib/GroupTheory/Perm/Finite.lean
theorem perm_mapsTo_inl_iff_mapsTo_inr {m n : Type*} [Finite m] [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)

Proof state:
case mp.inr
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)
x : m ⊕ n
r : n
hx : σ x = Sum.inr r
⊢ x ∈ Set.range Sum.inr → Sum.inr r ∈ Set.range Sum.inr

Tactic:
rintro _

Result:
case mp.inr
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)
x : m ⊕ n
r : n
hx : σ x = Sum.inr r
a✝ : x ∈ Set.range Sum.inr
⊢ Sum.inr r ∈ Set.range Sum.inr

Proof state:
case mp.inl.intro
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)
l : m
a : n
hx : σ (Sum.inr a) = Sum.inl l
⊢ Sum.inl l ∈ Set.range Sum.inr

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

Result:
case mp.inl.intro.intro
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)
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

Proof state:
case mpr
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑σ) (Set.range Sum.inr) (Set.range Sum.inr)
⊢ Set.MapsTo (⇑σ) (Set.range Sum.inl) (Set.range Sum.inl)

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

Result:
case mpr.inl
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ 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 mpr.inr
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ 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

Proof state:
case mpr.inr.intro.intro
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ 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

Tactic:
exact absurd hy Sum.inr_ne_inl

Result:
no goals

Proof state:
case mpr
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑σ⁻¹) (Set.range Sum.inr) (Set.range Sum.inr)
⊢ Set.MapsTo (⇑σ) (Set.range Sum.inl) (Set.range Sum.inl)

Tactic:
intro x

Result:
case mpr
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ 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

Proof state:
case mpr
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
⊢ Set.MapsTo (⇑σ) (Set.range Sum.inr) (Set.range Sum.inr) → Set.MapsTo (⇑σ) (Set.range Sum.inl) (Set.range Sum.inl)

Tactic:
intro h

Result:
case mpr
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑σ) (Set.range Sum.inr) (Set.range Sum.inr)
⊢ Set.MapsTo (⇑σ) (Set.range Sum.inl) (Set.range Sum.inl)

Proof state:
case mpr.inl
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ 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

Tactic:
rintro _

Result:
case mpr.inl
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ 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

Proof state:
case mpr.inr
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ 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

Tactic:
rintro ⟨a, rfl⟩

Result:
case mpr.inr.intro
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ 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

Proof state:
case mpr
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ 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

Tactic:
rcases hx : σ x with l | r

Result:
case mpr.inl
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ 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 mpr.inr
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ 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

Proof state:
case mpr.inl
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ 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

Tactic:
exact ⟨l, rfl⟩

Result:
no goals

Proof state:
case mp.inl
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)
x : m ⊕ n
l : m
hx : σ x = Sum.inl l
⊢ x ∈ Set.range Sum.inr → Sum.inl l ∈ Set.range Sum.inr

Tactic:
rintro ⟨a, rfl⟩

Result:
case mp.inl.intro
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)
l : m
a : n
hx : σ (Sum.inr a) = Sum.inl l
⊢ Sum.inl l ∈ Set.range Sum.inr

Proof state:
case mp.inl.intro.intro
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)
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

Tactic:
exact absurd hy Sum.inl_ne_inr

Result:
no goals

Proof state:
case mp.inr
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)
x : m ⊕ n
r : n
hx : σ x = Sum.inr r
a✝ : x ∈ Set.range Sum.inr
⊢ Sum.inr r ∈ Set.range Sum.inr

Tactic:
exact ⟨r, rfl⟩

Result:
no goals

Proof state:
case mpr.inr.intro.intro
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ 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

Tactic:
rw [← hx, σ.inv_apply_self] at hy

Result:
case mpr.inr.intro.intro
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ 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

Proof state:
case mpr
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑σ) (Set.range Sum.inr) (Set.range Sum.inr)
⊢ Set.MapsTo (⇑σ) (Set.range Sum.inl) (Set.range Sum.inl)

Tactic:
rw [← perm_inv_mapsTo_iff_mapsTo] at h

Result:
case mpr
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑σ⁻¹) (Set.range Sum.inr) (Set.range Sum.inr)
⊢ Set.MapsTo (⇑σ) (Set.range Sum.inl) (Set.range Sum.inl)