Theorem: Nat.Combination_compl_bijective (Jordan/MulActionCombination.lean)

State before:
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
⊢ Function.Bijective ⇑(Combination_compl G α hm)
Tactic:
constructor
State after:
case left
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
⊢ Function.Injective ⇑(Combination_compl G α hm)

case right
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
⊢ Function.Surjective ⇑(Combination_compl G α hm)

State before:
case left
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
⊢ Function.Injective ⇑(Combination_compl G α hm)
Tactic:
rintro ⟨s, hs⟩ ⟨t, ht⟩ h
State after:
case left.mk.mk
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : Finset α
hs : s ∈ Combination α n
t : Finset α
ht : t ∈ Combination α n
h : (Combination_compl G α hm) { val := s, property := hs } = (Combination_compl G α hm) { val := t, property := ht }
⊢ { val := s, property := hs } = { val := t, property := ht }

State before:
case left.mk.mk
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : Finset α
hs : s ∈ Combination α n
t : Finset α
ht : t ∈ Combination α n
h : (Combination_compl G α hm) { val := s, property := hs } = (Combination_compl G α hm) { val := t, property := ht }
⊢ { val := s, property := hs } = { val := t, property := ht }
Tactic:
rw [← Subtype.coe_inj] at h
State after:
case left.mk.mk
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : Finset α
hs : s ∈ Combination α n
t : Finset α
ht : t ∈ Combination α n
h :
  ↑((Combination_compl G α hm) { val := s, property := hs }) =
    ↑((Combination_compl G α hm) { val := t, property := ht })
⊢ { val := s, property := hs } = { val := t, property := ht }

State before:
case left.mk.mk
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : Finset α
hs : s ∈ Combination α n
t : Finset α
ht : t ∈ Combination α n
h :
  ↑((Combination_compl G α hm) { val := s, property := hs }) =
    ↑((Combination_compl G α hm) { val := t, property := ht })
⊢ { val := s, property := hs } = { val := t, property := ht }
Tactic:
change sᶜ = tᶜ at h
State after:
case left.mk.mk
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : Finset α
hs : s ∈ Combination α n
t : Finset α
ht : t ∈ Combination α n
h : sᶜ = tᶜ
⊢ { val := s, property := hs } = { val := t, property := ht }

State before:
case left.mk.mk
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : Finset α
hs : s ∈ Combination α n
t : Finset α
ht : t ∈ Combination α n
h : sᶜ = tᶜ
⊢ { val := s, property := hs } = { val := t, property := ht }
Tactic:
apply Subtype.coe_injective
State after:
case left.mk.mk.a
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : Finset α
hs : s ∈ Combination α n
t : Finset α
ht : t ∈ Combination α n
h : sᶜ = tᶜ
⊢ (fun a => ↑a) { val := s, property := hs } = (fun a => ↑a) { val := t, property := ht }

State before:
case left.mk.mk.a
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : Finset α
hs : s ∈ Combination α n
t : Finset α
ht : t ∈ Combination α n
h : sᶜ = tᶜ
⊢ (fun a => ↑a) { val := s, property := hs } = (fun a => ↑a) { val := t, property := ht }
Tactic:
change s = t
State after:
case left.mk.mk.a
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : Finset α
hs : s ∈ Combination α n
t : Finset α
ht : t ∈ Combination α n
h : sᶜ = tᶜ
⊢ s = t

State before:
case left.mk.mk.a
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : Finset α
hs : s ∈ Combination α n
t : Finset α
ht : t ∈ Combination α n
h : sᶜ = tᶜ
⊢ s = t
Tactic:
rw [← compl_compl s]
State after:
case left.mk.mk.a
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : Finset α
hs : s ∈ Combination α n
t : Finset α
ht : t ∈ Combination α n
h : sᶜ = tᶜ
⊢ sᶜᶜ = t

State before:
case left.mk.mk.a
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : Finset α
hs : s ∈ Combination α n
t : Finset α
ht : t ∈ Combination α n
h : sᶜ = tᶜ
⊢ sᶜᶜ = t
Tactic:
rw [h]
State after:
case left.mk.mk.a
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : Finset α
hs : s ∈ Combination α n
t : Finset α
ht : t ∈ Combination α n
h : sᶜ = tᶜ
⊢ tᶜᶜ = t

State before:
case left.mk.mk.a
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : Finset α
hs : s ∈ Combination α n
t : Finset α
ht : t ∈ Combination α n
h : sᶜ = tᶜ
⊢ tᶜᶜ = t
Tactic:
rw [compl_compl]
State after:
no goals

State before:
case right
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
⊢ Function.Surjective ⇑(Combination_compl G α hm)
Tactic:
rintro ⟨s, hs⟩
State after:
case right.mk
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : Finset α
hs : s ∈ Combination α m
⊢ ∃ a, (Combination_compl G α hm) a = { val := s, property := hs }

State before:
case right.mk
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : Finset α
hs : s ∈ Combination α m
⊢ ∃ a, (Combination_compl G α hm) a = { val := s, property := hs }
Tactic:
have hn : n + m = Fintype.card α := by rw [add_comm]; exact hm
State after:
case right.mk
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : Finset α
hs : s ∈ Combination α m
hn : n + m = Fintype.card α
⊢ ∃ a, (Combination_compl G α hm) a = { val := s, property := hs }

State before:
case right.mk
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : Finset α
hs : s ∈ Combination α m
hn : n + m = Fintype.card α
⊢ ∃ a, (Combination_compl G α hm) a = { val := s, property := hs }
Tactic:
use Nat.Combination_compl G α hn ⟨s, hs⟩
State after:
case h
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : Finset α
hs : s ∈ Combination α m
hn : n + m = Fintype.card α
⊢ (Combination_compl G α hm) ((Combination_compl G α hn) { val := s, property := hs }) = { val := s, property := hs }

State before:
case h
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : Finset α
hs : s ∈ Combination α m
hn : n + m = Fintype.card α
⊢ (Combination_compl G α hm) ((Combination_compl G α hn) { val := s, property := hs }) = { val := s, property := hs }
Tactic:
apply Subtype.coe_injective
State after:
case h.a
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : Finset α
hs : s ∈ Combination α m
hn : n + m = Fintype.card α
⊢ (fun a => ↑a) ((Combination_compl G α hm) ((Combination_compl G α hn) { val := s, property := hs })) =
    (fun a => ↑a) { val := s, property := hs }

State before:
case h.a
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : Finset α
hs : s ∈ Combination α m
hn : n + m = Fintype.card α
⊢ (fun a => ↑a) ((Combination_compl G α hm) ((Combination_compl G α hn) { val := s, property := hs })) =
    (fun a => ↑a) { val := s, property := hs }
Tactic:
change sᶜᶜ = s
State after:
case h.a
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : Finset α
hs : s ∈ Combination α m
hn : n + m = Fintype.card α
⊢ sᶜᶜ = s

State before:
case h.a
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : Finset α
hs : s ∈ Combination α m
hn : n + m = Fintype.card α
⊢ sᶜᶜ = s
Tactic:
rw [compl_compl]
State after:
no goals

State before:
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : Finset α
hs : s ∈ Combination α m
⊢ n + m = Fintype.card α
Tactic:
rw [add_comm]
State after:
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : Finset α
hs : s ∈ Combination α m
⊢ m + n = Fintype.card α

State before:
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : Finset α
hs : s ∈ Combination α m
⊢ m + n = Fintype.card α
Tactic:
exact hm
State after:
no goals