internlm/Lean-Github huggingface dataset:
Theorem: Nat.Combination_nontrivial
Proof 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
Proof 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)
Theorem: Nat.Combination_nontrivial
Proof 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)
Proof 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)
Theorem: Nat.Combination_nontrivial
Proof 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]
Proof 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
Theorem: Nat.Combination_nontrivial
Proof 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⟩
Proof 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
Theorem: Nat.Combination_nontrivial
Proof 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⟩
Proof 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 := ⋯ }
Theorem: Nat.Combination_nontrivial
Proof 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
Proof 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
Theorem: Nat.Combination_nontrivial
Proof 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
Proof 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
Theorem: Nat.Combination_nontrivial
Proof 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
Proof 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
Theorem: Nat.Combination_nontrivial
Proof 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]
Proof 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
Theorem: Nat.Combination_nontrivial
Proof 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 _
Proof state after:
no goals
Theorem: Nat.Combination_nontrivial
Proof 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]
Proof 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
Theorem: Nat.Combination_nontrivial
Proof 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]
Proof 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
Theorem: Nat.Combination_nontrivial
Proof 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]
Proof 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
Theorem: Nat.Combination_nontrivial
Proof 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]
Proof 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
Theorem: Nat.Combination_nontrivial
Proof 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]
Proof 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
Theorem: Nat.Combination_nontrivial
Proof 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
Proof 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
Theorem: Nat.Combination_nontrivial
Proof 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
Proof 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
Theorem: Nat.Combination_nontrivial
Proof 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
Proof 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
Theorem: Nat.Combination_nontrivial
Proof 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
Proof 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
⊢ α
Theorem: Nat.Combination_nontrivial
Proof 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
Proof state after:
no goals
Theorem: Nat.Combination_isPretransitive
Proof state before:
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
⊢ IsPretransitive (Equiv.Perm α) ↑(Combination α n)
Tactic:
apply Nat.Combination_isPretransitive_of_IsMultiplyPretransitive
Proof state after:
case h
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
⊢ IsMultiplyPretransitive (Equiv.Perm α) α n
Theorem: Nat.Combination_isPretransitive
Proof state before:
case h
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
⊢ IsMultiplyPretransitive (Equiv.Perm α) α n
Tactic:
apply Equiv.Perm.isMultiplyPretransitive
Proof state after:
no goals
Theorem: Nat.Combination_compl_bijective
Proof 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
Proof 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)
Theorem: Nat.Combination_compl_bijective
Proof 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
Proof 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 }
Theorem: Nat.Combination_compl_bijective
Proof 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
Proof 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 }
Theorem: Nat.Combination_compl_bijective
Proof 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
Proof 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 }
Theorem: Nat.Combination_compl_bijective
Proof 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
Proof 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 }
Theorem: Nat.Combination_compl_bijective
Proof 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
Proof 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
Theorem: Nat.Combination_compl_bijective
Proof 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]
Proof 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
Theorem: Nat.Combination_compl_bijective
Proof 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]
Proof 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
Theorem: Nat.Combination_compl_bijective
Proof 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]
Proof state after:
no goals
Theorem: Nat.Combination_compl_bijective
Proof 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⟩
Proof 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 }