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

State before:
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
⊢ Nontrivial ↑(Combination α n)
Tactic:
suffices Nonempty (n.Combination α) by
  obtain ⟨s, hs⟩ := this
  change s.card = n at hs
  let h'1 := id h1
  rw [← hs, Finset.card_pos] at h'1 ; obtain ⟨a, ha⟩ := h'1
  let h'2 := id h2
  rw [← hs, Finset.card_lt_iff_ne_univ, Ne.def, ← Finset.coe_eq_univ, ← Ne.def,
  Set.ne_univ_iff_exists_not_mem] at h'2
  obtain ⟨b, hb⟩ := h'2
  let t : Finset α := insert b (Finset.erase s a)
  rw [nontrivial_iff]
  use ⟨s, hs⟩
  use ⟨t, by
    rw [Nat.Combination.mem_iff]
    rw [Finset.card_insert_of_not_mem]
    rw [Finset.card_erase_of_mem ha]
    rw [hs]; rw [Nat.sub_add_cancel]; exact h1
    intro h; apply hb; apply Finset.erase_subset; exact h⟩
  intro h
  rw [Subtype.mk_eq_mk] at h
  apply hb
  rw [h]
  exact Finset.mem_insert_self b _
State after:
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
⊢ Nonempty ↑(Combination α n)

State before:
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
⊢ Nonempty ↑(Combination α n)
Tactic:
obtain ⟨s, _, hs'⟩ := Finset.exists_smaller_set (Finset.univ : Finset α) n
  (le_of_lt h2)
State after:
case intro.intro
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
left✝ : s ⊆ Finset.univ
hs' : s.card = n
⊢ Nonempty ↑(Combination α n)

State before:
case intro.intro
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
left✝ : s ⊆ Finset.univ
hs' : s.card = n
⊢ Nonempty ↑(Combination α n)
Tactic:
use s
State after:
case property
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
left✝ : s ⊆ Finset.univ
hs' : s.card = n
⊢ s ∈ Combination α n

State before:
case property
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
left✝ : s ⊆ Finset.univ
hs' : s.card = n
⊢ s ∈ Combination α n
Tactic:
exact hs'
State after:
no goals

State before:
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
this : Nonempty ↑(Combination α n)
⊢ Nontrivial ↑(Combination α n)
Tactic:
obtain ⟨s, hs⟩ := this
State after:
case intro.mk
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s ∈ Combination α n
⊢ Nontrivial ↑(Combination α n)

State before:
case intro.mk
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s ∈ Combination α n
⊢ Nontrivial ↑(Combination α n)
Tactic:
change s.card = n at hs
State after:
case intro.mk
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
⊢ Nontrivial ↑(Combination α n)

State before:
case intro.mk
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
⊢ Nontrivial ↑(Combination α n)
Tactic:
let h'1 := id h1
State after:
case intro.mk
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
h'1 : 0 < n := id h1
⊢ Nontrivial ↑(Combination α n)

State before:
case intro.mk
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
h'1 : 0 < n := id h1
⊢ Nontrivial ↑(Combination α n)
Tactic:
rw [← hs, Finset.card_pos] at h'1
State after:
case intro.mk
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
h'1 : s.Nonempty
⊢ Nontrivial ↑(Combination α n)

State before:
case intro.mk
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
h'1 : s.Nonempty
⊢ Nontrivial ↑(Combination α n)
Tactic:
obtain ⟨a, ha⟩ := h'1
State after:
case intro.mk.intro
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
⊢ Nontrivial ↑(Combination α n)

State before:
case intro.mk.intro
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
⊢ Nontrivial ↑(Combination α n)
Tactic:
let h'2 := id h2
State after:
case intro.mk.intro
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
h'2 : n < Fintype.card α := id h2
⊢ Nontrivial ↑(Combination α n)

State before:
case intro.mk.intro
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
h'2 : n < Fintype.card α := id h2
⊢ Nontrivial ↑(Combination α n)
Tactic:
rw [← hs, Finset.card_lt_iff_ne_univ, Ne.def, ← Finset.coe_eq_univ, ← Ne.def,
Set.ne_univ_iff_exists_not_mem] at h'2
State after:
case intro.mk.intro
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
h'2 : ∃ a, a ∉ ↑s
⊢ Nontrivial ↑(Combination α n)

State before:
case intro.mk.intro
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
h'2 : ∃ a, a ∉ ↑s
⊢ Nontrivial ↑(Combination α n)
Tactic:
obtain ⟨b, hb⟩ := h'2
State after:
case intro.mk.intro.intro
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
b : α
hb : b ∉ ↑s
⊢ Nontrivial ↑(Combination α n)

State before:
case intro.mk.intro.intro
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
b : α
hb : b ∉ ↑s
⊢ Nontrivial ↑(Combination α n)
Tactic:
let t : Finset α := insert b (Finset.erase s a)
State after:
case intro.mk.intro.intro
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
b : α
hb : b ∉ ↑s
t : Finset α := insert b (Finset.erase s a)
⊢ Nontrivial ↑(Combination α n)

State before:
case intro.mk.intro.intro
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
b : α
hb : b ∉ ↑s
t : Finset α := insert b (Finset.erase s a)
⊢ Nontrivial ↑(Combination α n)
Tactic:
rw [nontrivial_iff]
State after:
case intro.mk.intro.intro
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
b : α
hb : b ∉ ↑s
t : Finset α := insert b (Finset.erase s a)
⊢ ∃ x y, x ≠ y

State before:
case intro.mk.intro.intro
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
b : α
hb : b ∉ ↑s
t : Finset α := insert b (Finset.erase s a)
⊢ ∃ x y, x ≠ y
Tactic:
use ⟨s, hs⟩
State after:
case h
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
b : α
hb : b ∉ ↑s
t : Finset α := insert b (Finset.erase s a)
⊢ ∃ y, { val := s, property := hs } ≠ y

State before:
case h
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
b : α
hb : b ∉ ↑s
t : Finset α := insert b (Finset.erase s a)
⊢ ∃ y, { val := s, property := hs } ≠ y
Tactic:
use ⟨t, by
  rw [Nat.Combination.mem_iff]
  rw [Finset.card_insert_of_not_mem]
  rw [Finset.card_erase_of_mem ha]
  rw [hs]; rw [Nat.sub_add_cancel]; exact h1
  intro h; apply hb; apply Finset.erase_subset; exact h⟩
State after:
case h
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
b : α
hb : b ∉ ↑s
t : Finset α := insert b (Finset.erase s a)
⊢ { val := s, property := hs } ≠ { val := t, property := ⋯ }

State before:
case h
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
b : α
hb : b ∉ ↑s
t : Finset α := insert b (Finset.erase s a)
⊢ { val := s, property := hs } ≠ { val := t, property := ⋯ }
Tactic:
intro h
State after:
case h
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
b : α
hb : b ∉ ↑s
t : Finset α := insert b (Finset.erase s a)
h : { val := s, property := hs } = { val := t, property := ⋯ }
⊢ False

State before:
case h
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
b : α
hb : b ∉ ↑s
t : Finset α := insert b (Finset.erase s a)
h : { val := s, property := hs } = { val := t, property := ⋯ }
⊢ False
Tactic:
rw [Subtype.mk_eq_mk] at h
State after:
case h
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
b : α
hb : b ∉ ↑s
t : Finset α := insert b (Finset.erase s a)
h : s = t
⊢ False

State before:
case h
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
b : α
hb : b ∉ ↑s
t : Finset α := insert b (Finset.erase s a)
h : s = t
⊢ False
Tactic:
apply hb
State after:
case h
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
b : α
hb : b ∉ ↑s
t : Finset α := insert b (Finset.erase s a)
h : s = t
⊢ b ∈ ↑s

State before:
case h
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
b : α
hb : b ∉ ↑s
t : Finset α := insert b (Finset.erase s a)
h : s = t
⊢ b ∈ ↑s
Tactic:
rw [h]
State after:
case h
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
b : α
hb : b ∉ ↑s
t : Finset α := insert b (Finset.erase s a)
h : s = t
⊢ b ∈ ↑t

State before:
case h
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
b : α
hb : b ∉ ↑s
t : Finset α := insert b (Finset.erase s a)
h : s = t
⊢ b ∈ ↑t
Tactic:
exact Finset.mem_insert_self b _
State after:
no goals

State before:
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
b : α
hb : b ∉ ↑s
t : Finset α := insert b (Finset.erase s a)
⊢ t ∈ Combination α n
Tactic:
rw [Nat.Combination.mem_iff]
State after:
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
b : α
hb : b ∉ ↑s
t : Finset α := insert b (Finset.erase s a)
⊢ t.card = n

State before:
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
b : α
hb : b ∉ ↑s
t : Finset α := insert b (Finset.erase s a)
⊢ t.card = n
Tactic:
rw [Finset.card_insert_of_not_mem]
State after:
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
b : α
hb : b ∉ ↑s
t : Finset α := insert b (Finset.erase s a)
⊢ (Finset.erase s a).card + 1 = n

G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
b : α
hb : b ∉ ↑s
t : Finset α := insert b (Finset.erase s a)
⊢ b ∉ Finset.erase s a

State before:
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
b : α
hb : b ∉ ↑s
t : Finset α := insert b (Finset.erase s a)
⊢ (Finset.erase s a).card + 1 = n

G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
b : α
hb : b ∉ ↑s
t : Finset α := insert b (Finset.erase s a)
⊢ b ∉ Finset.erase s a
Tactic:
rw [Finset.card_erase_of_mem ha]
State after:
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
b : α
hb : b ∉ ↑s
t : Finset α := insert b (Finset.erase s a)
⊢ s.card - 1 + 1 = n

G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
b : α
hb : b ∉ ↑s
t : Finset α := insert b (Finset.erase s a)
⊢ b ∉ Finset.erase s a

State before:
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
b : α
hb : b ∉ ↑s
t : Finset α := insert b (Finset.erase s a)
⊢ s.card - 1 + 1 = n

G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
b : α
hb : b ∉ ↑s
t : Finset α := insert b (Finset.erase s a)
⊢ b ∉ Finset.erase s a
Tactic:
rw [hs]
State after:
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
b : α
hb : b ∉ ↑s
t : Finset α := insert b (Finset.erase s a)
⊢ n - 1 + 1 = n

G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
b : α
hb : b ∉ ↑s
t : Finset α := insert b (Finset.erase s a)
⊢ b ∉ Finset.erase s a

State before:
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
b : α
hb : b ∉ ↑s
t : Finset α := insert b (Finset.erase s a)
⊢ n - 1 + 1 = n

G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
b : α
hb : b ∉ ↑s
t : Finset α := insert b (Finset.erase s a)
⊢ b ∉ Finset.erase s a
Tactic:
rw [Nat.sub_add_cancel]
State after:
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
b : α
hb : b ∉ ↑s
t : Finset α := insert b (Finset.erase s a)
⊢ 1 ≤ n

G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
b : α
hb : b ∉ ↑s
t : Finset α := insert b (Finset.erase s a)
⊢ b ∉ Finset.erase s a

State before:
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
b : α
hb : b ∉ ↑s
t : Finset α := insert b (Finset.erase s a)
⊢ 1 ≤ n

G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
b : α
hb : b ∉ ↑s
t : Finset α := insert b (Finset.erase s a)
⊢ b ∉ Finset.erase s a
Tactic:
exact h1
State after:
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
b : α
hb : b ∉ ↑s
t : Finset α := insert b (Finset.erase s a)
⊢ b ∉ Finset.erase s a

State before:
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
b : α
hb : b ∉ ↑s
t : Finset α := insert b (Finset.erase s a)
⊢ b ∉ Finset.erase s a
Tactic:
intro h
State after:
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
b : α
hb : b ∉ ↑s
t : Finset α := insert b (Finset.erase s a)
h : b ∈ Finset.erase s a
⊢ False

State before:
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
b : α
hb : b ∉ ↑s
t : Finset α := insert b (Finset.erase s a)
h : b ∈ Finset.erase s a
⊢ False
Tactic:
apply hb
State after:
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
b : α
hb : b ∉ ↑s
t : Finset α := insert b (Finset.erase s a)
h : b ∈ Finset.erase s a
⊢ b ∈ ↑s

State before:
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
b : α
hb : b ∉ ↑s
t : Finset α := insert b (Finset.erase s a)
h : b ∈ Finset.erase s a
⊢ b ∈ ↑s
Tactic:
apply Finset.erase_subset
State after:
case a
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
b : α
hb : b ∉ ↑s
t : Finset α := insert b (Finset.erase s a)
h : b ∈ Finset.erase s a
⊢ b ∈ Finset.erase s ?a

case a
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
b : α
hb : b ∉ ↑s
t : Finset α := insert b (Finset.erase s a)
h : b ∈ Finset.erase s a
⊢ α

State before:
case a
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
b : α
hb : b ∉ ↑s
t : Finset α := insert b (Finset.erase s a)
h : b ∈ Finset.erase s a
⊢ b ∈ Finset.erase s ?a

case a
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
b : α
hb : b ∉ ↑s
t : Finset α := insert b (Finset.erase s a)
h : b ∈ Finset.erase s a
⊢ α
Tactic:
exact h
State after:
no goals