internlm/Lean-Github huggingface dataset:
Theorem: support_min_lt_inv_apply
Proof state before:
case intro
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
n : ℕ := Nat.find hf
hn : n = Nat.find hf
hn' : f n ≠ n
hn'' : n ≠ f⁻¹ n → n ≤ f⁻¹ n
⊢ n < f⁻¹ n
Tactic:
rw [ne_eq, ← Equiv.Perm.eq_inv_iff_eq] at hn'
Proof state after:
case intro
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
n : ℕ := Nat.find hf
hn : n = Nat.find hf
hn' : ¬n = f⁻¹ n
hn'' : n ≠ f⁻¹ n → n ≤ f⁻¹ n
⊢ n < f⁻¹ n
Theorem: support_min_lt_inv_apply
Proof state before:
case intro
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
n : ℕ := Nat.find hf
hn : n = Nat.find hf
hn' : ¬n = f⁻¹ n
hn'' : n ≠ f⁻¹ n → n ≤ f⁻¹ n
⊢ n < f⁻¹ n
Tactic:
apply lt_of_le_of_ne (hn'' hn') hn'
Proof state after:
no goals
Theorem: support_min_lt_apply
Proof state before:
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
⊢ Nat.find hf < f (Nat.find hf)
Tactic:
have hg : ∃ n, f⁻¹ n ≠ n
Proof state after:
case hg
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
⊢ ∃ n, f⁻¹ n ≠ n

f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
⊢ Nat.find hf < f (Nat.find hf)
Theorem: support_min_lt_apply
Proof state before:
case hg
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
⊢ ∃ n, f⁻¹ n ≠ n

f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
⊢ Nat.find hf < f (Nat.find hf)
Tactic:
. simp_rw [ne_comm, ne_eq, Equiv.Perm.eq_inv_iff_eq]
  exact hf
Proof state after:
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
⊢ Nat.find hf < f (Nat.find hf)
Theorem: support_min_lt_apply
Proof state before:
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
⊢ Nat.find hf < f (Nat.find hf)
Tactic:
have hf_finv : ∀ n, f n ≠ n ↔ f⁻¹ n ≠ n
Proof state after:
case hf_finv
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
⊢ ∀ (n : ℕ), f n ≠ n ↔ f⁻¹ n ≠ n

f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
hf_finv : ∀ (n : ℕ), f n ≠ n ↔ f⁻¹ n ≠ n
⊢ Nat.find hf < f (Nat.find hf)
Theorem: support_min_lt_apply
Proof state before:
case hf_finv
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
⊢ ∀ (n : ℕ), f n ≠ n ↔ f⁻¹ n ≠ n

f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
hf_finv : ∀ (n : ℕ), f n ≠ n ↔ f⁻¹ n ≠ n
⊢ Nat.find hf < f (Nat.find hf)
Tactic:
. simp_rw [ne_comm, ne_eq, Equiv.Perm.eq_inv_iff_eq, eq_comm]
  exact fun n ↦ trivial
Proof state after:
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
hf_finv : ∀ (n : ℕ), f n ≠ n ↔ f⁻¹ n ≠ n
⊢ Nat.find hf < f (Nat.find hf)
Theorem: support_min_lt_apply
Proof state before:
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
hf_finv : ∀ (n : ℕ), f n ≠ n ↔ f⁻¹ n ≠ n
⊢ Nat.find hf < f (Nat.find hf)
Tactic:
have key : Nat.find hf = Nat.find hg
Proof state after:
case key
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
hf_finv : ∀ (n : ℕ), f n ≠ n ↔ f⁻¹ n ≠ n
⊢ Nat.find hf = Nat.find hg

f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
hf_finv : ∀ (n : ℕ), f n ≠ n ↔ f⁻¹ n ≠ n
key : Nat.find hf = Nat.find hg
⊢ Nat.find hf < f (Nat.find hf)
Theorem: support_min_lt_apply
Proof state before:
case key
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
hf_finv : ∀ (n : ℕ), f n ≠ n ↔ f⁻¹ n ≠ n
⊢ Nat.find hf = Nat.find hg

f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
hf_finv : ∀ (n : ℕ), f n ≠ n ↔ f⁻¹ n ≠ n
key : Nat.find hf = Nat.find hg
⊢ Nat.find hf < f (Nat.find hf)
Tactic:
. simp_rw [Nat.find_eq_iff, hf_finv, ← Nat.find_eq_iff hg]
Proof state after:
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
hf_finv : ∀ (n : ℕ), f n ≠ n ↔ f⁻¹ n ≠ n
key : Nat.find hf = Nat.find hg
⊢ Nat.find hf < f (Nat.find hf)
Theorem: support_min_lt_apply
Proof state before:
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
hf_finv : ∀ (n : ℕ), f n ≠ n ↔ f⁻¹ n ≠ n
key : Nat.find hf = Nat.find hg
⊢ Nat.find hf < f (Nat.find hf)
Tactic:
rw [key]
Proof state after:
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
hf_finv : ∀ (n : ℕ), f n ≠ n ↔ f⁻¹ n ≠ n
key : Nat.find hf = Nat.find hg
⊢ Nat.find hg < f (Nat.find hg)
Theorem: support_min_lt_apply
Proof state before:
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
hf_finv : ∀ (n : ℕ), f n ≠ n ↔ f⁻¹ n ≠ n
key : Nat.find hf = Nat.find hg
⊢ Nat.find hg < f (Nat.find hg)
Tactic:
have := support_min_lt_inv_apply f⁻¹ hg
Proof state after:
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
hf_finv : ∀ (n : ℕ), f n ≠ n ↔ f⁻¹ n ≠ n
key : Nat.find hf = Nat.find hg
this : Nat.find hg < f⁻¹⁻¹ (Nat.find hg)
⊢ Nat.find hg < f (Nat.find hg)
Theorem: support_min_lt_apply
Proof state before:
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
hf_finv : ∀ (n : ℕ), f n ≠ n ↔ f⁻¹ n ≠ n
key : Nat.find hf = Nat.find hg
this : Nat.find hg < f⁻¹⁻¹ (Nat.find hg)
⊢ Nat.find hg < f (Nat.find hg)
Tactic:
rw [inv_inv] at this
Proof state after:
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
hf_finv : ∀ (n : ℕ), f n ≠ n ↔ f⁻¹ n ≠ n
key : Nat.find hf = Nat.find hg
this : Nat.find hg < f (Nat.find hg)
⊢ Nat.find hg < f (Nat.find hg)
Theorem: support_min_lt_apply
Proof state before:
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
hf_finv : ∀ (n : ℕ), f n ≠ n ↔ f⁻¹ n ≠ n
key : Nat.find hf = Nat.find hg
this : Nat.find hg < f (Nat.find hg)
⊢ Nat.find hg < f (Nat.find hg)
Tactic:
exact this
Proof state after:
no goals
Theorem: support_min_lt_apply
Proof state before:
case hg
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
⊢ ∃ n, f⁻¹ n ≠ n
Tactic:
simp_rw [ne_comm, ne_eq, Equiv.Perm.eq_inv_iff_eq]
Proof state after:
case hg
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
⊢ ∃ n, ¬f n = n
Theorem: support_min_lt_apply
Proof state before:
case hg
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
⊢ ∃ n, ¬f n = n
Tactic:
exact hf
Proof state after:
no goals
Theorem: support_min_lt_apply
Proof state before:
case hf_finv
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
⊢ ∀ (n : ℕ), f n ≠ n ↔ f⁻¹ n ≠ n
Tactic:
simp_rw [ne_comm, ne_eq, Equiv.Perm.eq_inv_iff_eq, eq_comm]
Proof state after:
case hf_finv
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
⊢ ℕ → True
Theorem: support_min_lt_apply
Proof state before:
case hf_finv
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
⊢ ℕ → True
Tactic:
exact fun n ↦ trivial
Proof state after:
no goals
Theorem: support_min_lt_apply
Proof state before:
case key
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
hf_finv : ∀ (n : ℕ), f n ≠ n ↔ f⁻¹ n ≠ n
⊢ Nat.find hf = Nat.find hg
Tactic:
simp_rw [Nat.find_eq_iff, hf_finv, ← Nat.find_eq_iff hg]
Proof state after:
no goals
Theorem: support_empty_iff_id
Proof state before:
α : Type u_1
f : Equiv.Perm α
⊢ support f = ∅ ↔ f = 1
Tactic:
simp only [Set.eq_empty_iff_forall_not_mem, support,
            ne_eq, Set.mem_setOf_eq, not_not]
Proof state after:
α : Type u_1
f : Equiv.Perm α
⊢ (∀ (x : α), f x = x) ↔ f = 1
Theorem: support_empty_iff_id
Proof state before:
α : Type u_1
f : Equiv.Perm α
⊢ (∀ (x : α), f x = x) ↔ f = 1
Tactic:
exact Iff.symm Equiv.ext_iff
Proof state after:
no goals
Theorem: unswap_support
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
f : Equiv.Perm α
a : α
⊢ a ∉ support (Equiv.swap a (f a) * f)
Tactic:
simp [support] at *
Proof state after:
no goals
Theorem: unswap_support'
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
f : Equiv.Perm α
a : α
⊢ support (Equiv.swap a (f a) * f) ⊆ support f
Tactic:
simp [support] at *
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
f : Equiv.Perm α
a : α
⊢ ∀ (a_1 : α), ¬(Equiv.swap a (f a)) (f a_1) = a_1 → ¬f a_1 = a_1
Theorem: unswap_support'
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
f : Equiv.Perm α
a : α
⊢ ∀ (a_1 : α), ¬(Equiv.swap a (f a)) (f a_1) = a_1 → ¬f a_1 = a_1
Tactic:
intro b
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
f : Equiv.Perm α
a b : α
⊢ ¬(Equiv.swap a (f a)) (f b) = b → ¬f b = b
Theorem: unswap_support'
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
f : Equiv.Perm α
a b : α
⊢ ¬(Equiv.swap a (f a)) (f b) = b → ¬f b = b
Tactic:
contrapose!
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
f : Equiv.Perm α
a b : α
⊢ f b = b → (Equiv.swap a (f a)) (f b) = b
Theorem: unswap_support'
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
f : Equiv.Perm α
a b : α
⊢ f b = b → (Equiv.swap a (f a)) (f b) = b
Tactic:
intro hbf
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
f : Equiv.Perm α
a b : α
hbf : f b = b
⊢ (Equiv.swap a (f a)) (f b) = b
Theorem: unswap_support'
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
f : Equiv.Perm α
a b : α
hbf : f b = b
⊢ (Equiv.swap a (f a)) (f b) = b
Tactic:
rw [hbf]
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
f : Equiv.Perm α
a b : α
hbf : f b = b
⊢ (Equiv.swap a (f a)) b = b
Theorem: unswap_support'
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
f : Equiv.Perm α
a b : α
hbf : f b = b
⊢ (Equiv.swap a (f a)) b = b
Tactic:
by_cases h : b = a
Proof state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
f : Equiv.Perm α
a b : α
hbf : f b = b
h : b = a
⊢ (Equiv.swap a (f a)) b = b

case neg
α : Type u_1
inst✝ : DecidableEq α
f : Equiv.Perm α
a b : α
hbf : f b = b
h : ¬b = a
⊢ (Equiv.swap a (f a)) b = b
Theorem: unswap_support'
Proof state before:
case pos
α : Type u_1
inst✝ : DecidableEq α
f : Equiv.Perm α
a b : α
hbf : f b = b
h : b = a
⊢ (Equiv.swap a (f a)) b = b

case neg
α : Type u_1
inst✝ : DecidableEq α
f : Equiv.Perm α
a b : α
hbf : f b = b
h : ¬b = a
⊢ (Equiv.swap a (f a)) b = b
Tactic:
. subst b
  simp [hbf]
Proof state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
f : Equiv.Perm α
a b : α
hbf : f b = b
h : ¬b = a
⊢ (Equiv.swap a (f a)) b = b
Theorem: unswap_support'
Proof state before:
case neg
α : Type u_1
inst✝ : DecidableEq α
f : Equiv.Perm α
a b : α
hbf : f b = b
h : ¬b = a
⊢ (Equiv.swap a (f a)) b = b
Tactic:
by_cases h' : b = f a
Proof state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
f : Equiv.Perm α
a b : α
hbf : f b = b
h : ¬b = a
h' : b = f a
⊢ (Equiv.swap a (f a)) b = b

case neg
α : Type u_1
inst✝ : DecidableEq α
f : Equiv.Perm α
a b : α
hbf : f b = b
h : ¬b = a
h' : ¬b = f a
⊢ (Equiv.swap a (f a)) b = b
Theorem: unswap_support'
Proof state before:
case pos
α : Type u_1
inst✝ : DecidableEq α
f : Equiv.Perm α
a b : α
hbf : f b = b
h : ¬b = a
h' : b = f a
⊢ (Equiv.swap a (f a)) b = b

case neg
α : Type u_1
inst✝ : DecidableEq α
f : Equiv.Perm α
a b : α
hbf : f b = b
h : ¬b = a
h' : ¬b = f a
⊢ (Equiv.swap a (f a)) b = b
Tactic:
. subst b
  simp
  apply f.injective hbf.symm
Proof state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
f : Equiv.Perm α
a b : α
hbf : f b = b
h : ¬b = a
h' : ¬b = f a
⊢ (Equiv.swap a (f a)) b = b
Theorem: unswap_support'
Proof state before:
case neg
α : Type u_1
inst✝ : DecidableEq α
f : Equiv.Perm α
a b : α
hbf : f b = b
h : ¬b = a
h' : ¬b = f a
⊢ (Equiv.swap a (f a)) b = b
Tactic:
apply Equiv.swap_apply_of_ne_of_ne h h'
Proof state after:
no goals
Theorem: unswap_support'
Proof state before:
case pos
α : Type u_1
inst✝ : DecidableEq α
f : Equiv.Perm α
a b : α
hbf : f b = b
h : b = a
⊢ (Equiv.swap a (f a)) b = b
Tactic:
subst b
Proof state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
f : Equiv.Perm α
a : α
hbf : f a = a
⊢ (Equiv.swap a (f a)) a = a
Theorem: unswap_support'
Proof state before:
case pos
α : Type u_1
inst✝ : DecidableEq α
f : Equiv.Perm α
a : α
hbf : f a = a
⊢ (Equiv.swap a (f a)) a = a
Tactic:
simp [hbf]
Proof state after:
no goals
Theorem: unswap_support'
Proof state before:
case pos
α : Type u_1
inst✝ : DecidableEq α
f : Equiv.Perm α
a b : α
hbf : f b = b
h : ¬b = a
h' : b = f a
⊢ (Equiv.swap a (f a)) b = b
Tactic:
subst b
Proof state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
f : Equiv.Perm α
a : α
hbf : f (f a) = f a
h : ¬f a = a
⊢ (Equiv.swap a (f a)) (f a) = f a
Theorem: unswap_support'
Proof state before:
case pos
α : Type u_1
inst✝ : DecidableEq α
f : Equiv.Perm α
a : α
hbf : f (f a) = f a
h : ¬f a = a
⊢ (Equiv.swap a (f a)) (f a) = f a
Tactic:
simp
Proof state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
f : Equiv.Perm α
a : α
hbf : f (f a) = f a
h : ¬f a = a
⊢ a = f a
Theorem: unswap_support'
Proof state before:
case pos
α : Type u_1
inst✝ : DecidableEq α
f : Equiv.Perm α
a : α
hbf : f (f a) = f a
h : ¬f a = a
⊢ a = f a
Tactic:
apply f.injective hbf.symm
Proof state after:
no goals
Theorem: repbleByWord_aux
Proof state before:
s : Set ℕ
hs : Set.Finite s
⊢ RepbleByWord_aux s
Tactic:
apply @Set.Finite.induction_on _ RepbleByWord_aux _ hs
Proof state after:
case H0
s : Set ℕ
hs : Set.Finite s
⊢ RepbleByWord_aux ∅

case H1
s : Set ℕ
hs : Set.Finite s
⊢ ∀ {a : ℕ} {s : Set ℕ}, a ∉ s → Set.Finite s → RepbleByWord_aux s → RepbleByWord_aux (insert a s)
Theorem: repbleByWord_aux
Proof state before:
case H0
s : Set ℕ
hs : Set.Finite s
⊢ RepbleByWord_aux ∅

case H1
s : Set ℕ
hs : Set.Finite s
⊢ ∀ {a : ℕ} {s : Set ℕ}, a ∉ s → Set.Finite s → RepbleByWord_aux s → RepbleByWord_aux (insert a s)
Tactic:
all_goals clear s hs
Proof state after:
case H0

⊢ RepbleByWord_aux ∅

case H1

⊢ ∀ {a : ℕ} {s : Set ℕ}, a ∉ s → Set.Finite s → RepbleByWord_aux s → RepbleByWord_aux (insert a s)
Theorem: repbleByWord_aux
Proof state before:
case H0

⊢ RepbleByWord_aux ∅

case H1

⊢ ∀ {a : ℕ} {s : Set ℕ}, a ∉ s → Set.Finite s → RepbleByWord_aux s → RepbleByWord_aux (insert a s)
Tactic:
. intros f hf
  rw [Set.subset_empty_iff, support_empty_iff_id] at hf
  subst hf
  exact ⟨_, idHasWord⟩
Proof state after:
case H1

⊢ ∀ {a : ℕ} {s : Set ℕ}, a ∉ s → Set.Finite s → RepbleByWord_aux s → RepbleByWord_aux (insert a s)
Theorem: repbleByWord_aux
Proof state before:
case H1

⊢ ∀ {a : ℕ} {s : Set ℕ}, a ∉ s → Set.Finite s → RepbleByWord_aux s → RepbleByWord_aux (insert a s)
Tactic:
. intros a s _ _ hs_repble f hf
  set g := (Equiv.swap a (f a)) * f with hg
  suffices hgs : support g ⊆ s
  obtain ⟨w, hw⟩ := hs_repble g hgs
  obtain ⟨w_swap, hw_swap⟩ := swapHasWord a (f a)
  use (w_swap ++ w)
  simp [Word_mul, hw_swap, hw, hg]
  . intro b hb
    by_cases h : b = a
    . subst b
      absurd (unswap_support f a)
      exact hb
    exact Set.mem_of_mem_insert_of_ne (hf (unswap_support' _ _ hb)) h
Proof state after:
no goals
Theorem: repbleByWord_aux
Proof state before:
case H1
s : Set ℕ
hs : Set.Finite s
⊢ ∀ {a : ℕ} {s : Set ℕ}, a ∉ s → Set.Finite s → RepbleByWord_aux s → RepbleByWord_aux (insert a s)
Tactic:
clear s hs
Proof state after:
case H1

⊢ ∀ {a : ℕ} {s : Set ℕ}, a ∉ s → Set.Finite s → RepbleByWord_aux s → RepbleByWord_aux (insert a s)
Theorem: repbleByWord_aux
Proof state before:
case H0

⊢ RepbleByWord_aux ∅
Tactic:
intros f hf
Proof state after:
case H0
f : Equiv.Perm ℕ
hf : support f ⊆ ∅
⊢ RepbleByWord f
Theorem: repbleByWord_aux
Proof state before:
case H0
f : Equiv.Perm ℕ
hf : support f ⊆ ∅
⊢ RepbleByWord f
Tactic:
rw [Set.subset_empty_iff, support_empty_iff_id] at hf
Proof state after:
case H0
f : Equiv.Perm ℕ
hf : f = 1
⊢ RepbleByWord f
Theorem: repbleByWord_aux
Proof state before:
case H0
f : Equiv.Perm ℕ
hf : f = 1
⊢ RepbleByWord f
Tactic:
subst hf
Proof state after:
case H0

⊢ RepbleByWord 1
Theorem: repbleByWord_aux
Proof state before:
case H0

⊢ RepbleByWord 1
Tactic:
exact ⟨_, idHasWord⟩
Proof state after:
no goals
Theorem: repbleByWord_aux
Proof state before:
case H1

⊢ ∀ {a : ℕ} {s : Set ℕ}, a ∉ s → Set.Finite s → RepbleByWord_aux s → RepbleByWord_aux (insert a s)
Tactic:
intros a s _ _ hs_repble f hf
Proof state after:
case H1
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
⊢ RepbleByWord f
Theorem: repbleByWord_aux
Proof state before:
case H1
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
⊢ RepbleByWord f
Tactic:
set g := (Equiv.swap a (f a)) * f with hg
Proof state after:
case H1
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
⊢ RepbleByWord f
Theorem: repbleByWord_aux
Proof state before:
case H1
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
⊢ RepbleByWord f
Tactic:
suffices hgs : support g ⊆ s
Proof state after:
case H1
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
hgs : support g ⊆ s
⊢ RepbleByWord f

case hgs
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
⊢ support g ⊆ s
Theorem: repbleByWord_aux
Proof state before:
case H1
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
hgs : support g ⊆ s
⊢ RepbleByWord f

case hgs
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
⊢ support g ⊆ s
Tactic:
obtain ⟨w, hw⟩ := hs_repble g hgs
Proof state after:
case H1.intro
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
hgs : support g ⊆ s
w : Word
hw : Word.toPerm w = g
⊢ RepbleByWord f

case hgs
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
⊢ support g ⊆ s
Theorem: repbleByWord_aux
Proof state before:
case H1.intro
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
hgs : support g ⊆ s
w : Word
hw : Word.toPerm w = g
⊢ RepbleByWord f

case hgs
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
⊢ support g ⊆ s
Tactic:
obtain ⟨w_swap, hw_swap⟩ := swapHasWord a (f a)
Proof state after:
case H1.intro.intro
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
hgs : support g ⊆ s
w : Word
hw : Word.toPerm w = g
w_swap : Word
hw_swap : Word.toPerm w_swap = Equiv.swap a (f a)
⊢ RepbleByWord f

case hgs
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
⊢ support g ⊆ s
Theorem: repbleByWord_aux
Proof state before:
case H1.intro.intro
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
hgs : support g ⊆ s
w : Word
hw : Word.toPerm w = g
w_swap : Word
hw_swap : Word.toPerm w_swap = Equiv.swap a (f a)
⊢ RepbleByWord f

case hgs
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
⊢ support g ⊆ s
Tactic:
use (w_swap ++ w)
Proof state after:
case h
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
hgs : support g ⊆ s
w : Word
hw : Word.toPerm w = g
w_swap : Word
hw_swap : Word.toPerm w_swap = Equiv.swap a (f a)
⊢ Word.toPerm (w_swap ++ w) = f

case hgs
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
⊢ support g ⊆ s
Theorem: repbleByWord_aux
Proof state before:
case h
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
hgs : support g ⊆ s
w : Word
hw : Word.toPerm w = g
w_swap : Word
hw_swap : Word.toPerm w_swap = Equiv.swap a (f a)
⊢ Word.toPerm (w_swap ++ w) = f

case hgs
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
⊢ support g ⊆ s
Tactic:
simp [Word_mul, hw_swap, hw, hg]
Proof state after:
case hgs
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
⊢ support g ⊆ s
Theorem: repbleByWord_aux
Proof state before:
case hgs
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
⊢ support g ⊆ s
Tactic:
. intro b hb
  by_cases h : b = a
  . subst b
    absurd (unswap_support f a)
    exact hb
  exact Set.mem_of_mem_insert_of_ne (hf (unswap_support' _ _ hb)) h
Proof state after:
no goals
Theorem: repbleByWord_aux
Proof state before:
case hgs
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
⊢ support g ⊆ s
Tactic:
intro b hb
Proof state after:
case hgs
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
b : ℕ
hb : b ∈ support g
⊢ b ∈ s
Theorem: repbleByWord_aux
Proof state before:
case hgs
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
b : ℕ
hb : b ∈ support g
⊢ b ∈ s
Tactic:
by_cases h : b = a
Proof state after:
case pos
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
b : ℕ
hb : b ∈ support g
h : b = a
⊢ b ∈ s

case neg
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
b : ℕ
hb : b ∈ support g
h : ¬b = a
⊢ b ∈ s
Theorem: repbleByWord_aux
Proof state before:
case pos
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
b : ℕ
hb : b ∈ support g
h : b = a
⊢ b ∈ s

case neg
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
b : ℕ
hb : b ∈ support g
h : ¬b = a
⊢ b ∈ s
Tactic:
. subst b
  absurd (unswap_support f a)
  exact hb
Proof state after:
case neg
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
b : ℕ
hb : b ∈ support g
h : ¬b = a
⊢ b ∈ s
Theorem: repbleByWord_aux
Proof state before:
case neg
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
b : ℕ
hb : b ∈ support g
h : ¬b = a
⊢ b ∈ s
Tactic:
exact Set.mem_of_mem_insert_of_ne (hf (unswap_support' _ _ hb)) h
Proof state after:
no goals