internlm/Lean-Github huggingface dataset:
Theorem: Classical.InvFreeSets.chains_bounded_above
Proof state before:
case h
X : Type u_1
inst✝ : ProperInvolutiveInv X
c : Set (InvFreeSets X)
hcChain : IsChain LE.le c
sup : InvFreeSets X := chainUnion c hcChain
A : InvFreeSets X
hAc : A ∈ c
x : X
hxA : x ∈ ↑A
⊢ ↑A ∈ Set.range fun i => ⋃ i_1, ⋃ (_ : i_1 ∈ c ∧ ↑i_1 = i), i
Tactic:
use A
Proof state after:
case h
X : Type u_1
inst✝ : ProperInvolutiveInv X
c : Set (InvFreeSets X)
hcChain : IsChain LE.le c
sup : InvFreeSets X := chainUnion c hcChain
A : InvFreeSets X
hAc : A ∈ c
x : X
hxA : x ∈ ↑A
⊢ (fun i => ⋃ i_1, ⋃ (_ : i_1 ∈ c ∧ ↑i_1 = i), i) ↑A = ↑A
Theorem: Classical.InvFreeSets.chains_bounded_above
Proof state before:
case h
X : Type u_1
inst✝ : ProperInvolutiveInv X
c : Set (InvFreeSets X)
hcChain : IsChain LE.le c
sup : InvFreeSets X := chainUnion c hcChain
A : InvFreeSets X
hAc : A ∈ c
x : X
hxA : x ∈ ↑A
⊢ (fun i => ⋃ i_1, ⋃ (_ : i_1 ∈ c ∧ ↑i_1 = i), i) ↑A = ↑A
Tactic:
dsimp
Proof state after:
case h
X : Type u_1
inst✝ : ProperInvolutiveInv X
c : Set (InvFreeSets X)
hcChain : IsChain LE.le c
sup : InvFreeSets X := chainUnion c hcChain
A : InvFreeSets X
hAc : A ∈ c
x : X
hxA : x ∈ ↑A
⊢ ⋃ i, ⋃ (_ : i ∈ c ∧ ↑i = ↑A), ↑A = ↑A
Theorem: Classical.InvFreeSets.chains_bounded_above
Proof state before:
case h
X : Type u_1
inst✝ : ProperInvolutiveInv X
c : Set (InvFreeSets X)
hcChain : IsChain LE.le c
sup : InvFreeSets X := chainUnion c hcChain
A : InvFreeSets X
hAc : A ∈ c
x : X
hxA : x ∈ ↑A
⊢ ⋃ i, ⋃ (_ : i ∈ c ∧ ↑i = ↑A), ↑A = ↑A
Tactic:
ext
Proof state after:
case h.h
X : Type u_1
inst✝ : ProperInvolutiveInv X
c : Set (InvFreeSets X)
hcChain : IsChain LE.le c
sup : InvFreeSets X := chainUnion c hcChain
A : InvFreeSets X
hAc : A ∈ c
x : X
hxA : x ∈ ↑A
x✝ : X
⊢ x✝ ∈ ⋃ i, ⋃ (_ : i ∈ c ∧ ↑i = ↑A), ↑A ↔ x✝ ∈ ↑A
Theorem: Classical.InvFreeSets.chains_bounded_above
Proof state before:
case h.h
X : Type u_1
inst✝ : ProperInvolutiveInv X
c : Set (InvFreeSets X)
hcChain : IsChain LE.le c
sup : InvFreeSets X := chainUnion c hcChain
A : InvFreeSets X
hAc : A ∈ c
x : X
hxA : x ∈ ↑A
x✝ : X
⊢ x✝ ∈ ⋃ i, ⋃ (_ : i ∈ c ∧ ↑i = ↑A), ↑A ↔ x✝ ∈ ↑A
Tactic:
simp
Proof state after:
case h.h
X : Type u_1
inst✝ : ProperInvolutiveInv X
c : Set (InvFreeSets X)
hcChain : IsChain LE.le c
sup : InvFreeSets X := chainUnion c hcChain
A : InvFreeSets X
hAc : A ∈ c
x : X
hxA : x ∈ ↑A
x✝ : X
⊢ x✝ ∈ ↑A → InvFreeSet ↑A ∧ A ∈ c
Theorem: Classical.InvFreeSets.chains_bounded_above
Proof state before:
case h.h
X : Type u_1
inst✝ : ProperInvolutiveInv X
c : Set (InvFreeSets X)
hcChain : IsChain LE.le c
sup : InvFreeSets X := chainUnion c hcChain
A : InvFreeSets X
hAc : A ∈ c
x : X
hxA : x ∈ ↑A
x✝ : X
⊢ x✝ ∈ ↑A → InvFreeSet ↑A ∧ A ∈ c
Tactic:
intro
Proof state after:
case h.h
X : Type u_1
inst✝ : ProperInvolutiveInv X
c : Set (InvFreeSets X)
hcChain : IsChain LE.le c
sup : InvFreeSets X := chainUnion c hcChain
A : InvFreeSets X
hAc : A ∈ c
x : X
hxA : x ∈ ↑A
x✝ : X
a✝ : x✝ ∈ ↑A
⊢ InvFreeSet ↑A ∧ A ∈ c
Theorem: Classical.InvFreeSets.chains_bounded_above
Proof state before:
case h.h
X : Type u_1
inst✝ : ProperInvolutiveInv X
c : Set (InvFreeSets X)
hcChain : IsChain LE.le c
sup : InvFreeSets X := chainUnion c hcChain
A : InvFreeSets X
hAc : A ∈ c
x : X
hxA : x ∈ ↑A
x✝ : X
a✝ : x✝ ∈ ↑A
⊢ InvFreeSet ↑A ∧ A ∈ c
Tactic:
exact ⟨A.prop, hAc⟩
Proof state after:
no goals
Theorem: Classical.ProperInvolutiveInv.maxInvFreeSet_mem_inv
Proof state before:
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
⊢ x ∉ ↑(maxInvFreeSet X) → x⁻¹ ∈ ↑(maxInvFreeSet X)
Tactic:
intro h
Proof state after:
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h : x ∉ ↑(maxInvFreeSet X)
⊢ x⁻¹ ∈ ↑(maxInvFreeSet X)
Theorem: Classical.ProperInvolutiveInv.maxInvFreeSet_mem_inv
Proof state before:
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h : x ∉ ↑(maxInvFreeSet X)
C : InvFreeSets X :=
  { val := Set.insert x⁻¹ ↑(maxInvFreeSet X), property := (_ : InvFreeSet (Set.insert x⁻¹ ↑(maxInvFreeSet X))) }
⊢ x⁻¹ ∈ ↑(maxInvFreeSet X)
Tactic:
have : (maxInvFreeSet X).val ⊆ C.val := by
  show (maxInvFreeSet X).val ⊆ (maxInvFreeSet X).val.insert x⁻¹
  intro _; aesop (add norm simp [Set.insert])
Proof state after:
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h : x ∉ ↑(maxInvFreeSet X)
C : InvFreeSets X :=
  { val := Set.insert x⁻¹ ↑(maxInvFreeSet X), property := (_ : InvFreeSet (Set.insert x⁻¹ ↑(maxInvFreeSet X))) }
this : ↑(maxInvFreeSet X) ⊆ ↑C
⊢ x⁻¹ ∈ ↑(maxInvFreeSet X)
Theorem: Classical.ProperInvolutiveInv.maxInvFreeSet_mem_inv
Proof state before:
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h : x ∉ ↑(maxInvFreeSet X)
C : InvFreeSets X :=
  { val := Set.insert x⁻¹ ↑(maxInvFreeSet X), property := (_ : InvFreeSet (Set.insert x⁻¹ ↑(maxInvFreeSet X))) }
this : ↑(maxInvFreeSet X) ⊆ ↑C
⊢ x⁻¹ ∈ ↑(maxInvFreeSet X)
Tactic:
have := maxInvFreeSet_spec C this
Proof state after:
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h : x ∉ ↑(maxInvFreeSet X)
C : InvFreeSets X :=
  { val := Set.insert x⁻¹ ↑(maxInvFreeSet X), property := (_ : InvFreeSet (Set.insert x⁻¹ ↑(maxInvFreeSet X))) }
this✝ : ↑(maxInvFreeSet X) ⊆ ↑C
this : C = maxInvFreeSet X
⊢ x⁻¹ ∈ ↑(maxInvFreeSet X)
Theorem: Classical.ProperInvolutiveInv.maxInvFreeSet_mem_inv
Proof state before:
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h : x ∉ ↑(maxInvFreeSet X)
C : InvFreeSets X :=
  { val := Set.insert x⁻¹ ↑(maxInvFreeSet X), property := (_ : InvFreeSet (Set.insert x⁻¹ ↑(maxInvFreeSet X))) }
this✝ : ↑(maxInvFreeSet X) ⊆ ↑C
this : C = maxInvFreeSet X
⊢ x⁻¹ ∈ ↑(maxInvFreeSet X)
Tactic:
rw [← this]
Proof state after:
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h : x ∉ ↑(maxInvFreeSet X)
C : InvFreeSets X :=
  { val := Set.insert x⁻¹ ↑(maxInvFreeSet X), property := (_ : InvFreeSet (Set.insert x⁻¹ ↑(maxInvFreeSet X))) }
this✝ : ↑(maxInvFreeSet X) ⊆ ↑C
this : C = maxInvFreeSet X
⊢ x⁻¹ ∈ ↑C
Theorem: Classical.ProperInvolutiveInv.maxInvFreeSet_mem_inv
Proof state before:
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h : x ∉ ↑(maxInvFreeSet X)
C : InvFreeSets X :=
  { val := Set.insert x⁻¹ ↑(maxInvFreeSet X), property := (_ : InvFreeSet (Set.insert x⁻¹ ↑(maxInvFreeSet X))) }
this✝ : ↑(maxInvFreeSet X) ⊆ ↑C
this : C = maxInvFreeSet X
⊢ x⁻¹ ∈ ↑C
Tactic:
simp only [Set.insert, Set.mem_setOf_eq, true_or]
Proof state after:
no goals
Theorem: Classical.ProperInvolutiveInv.maxInvFreeSet_mem_inv
Proof state before:
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h : x ∉ ↑(maxInvFreeSet X)
⊢ InvFreeSet (Set.insert x⁻¹ ↑(maxInvFreeSet X))
Tactic:
simp only [Set.insert]
Proof state after:
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h : x ∉ ↑(maxInvFreeSet X)
⊢ InvFreeSet {b | b = x⁻¹ ∨ b ∈ ↑(maxInvFreeSet X)}
Theorem: Classical.ProperInvolutiveInv.maxInvFreeSet_mem_inv
Proof state before:
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h : x ∉ ↑(maxInvFreeSet X)
⊢ InvFreeSet {b | b = x⁻¹ ∨ b ∈ ↑(maxInvFreeSet X)}
Tactic:
intro a h
Proof state after:
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h✝ : x ∉ ↑(maxInvFreeSet X)
a : X
h : a ∈ {b | b = x⁻¹ ∨ b ∈ ↑(maxInvFreeSet X)}
⊢ a⁻¹ ∉ {b | b = x⁻¹ ∨ b ∈ ↑(maxInvFreeSet X)}
Theorem: Classical.ProperInvolutiveInv.maxInvFreeSet_mem_inv
Proof state before:
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h✝ : x ∉ ↑(maxInvFreeSet X)
a : X
h : a ∈ {b | b = x⁻¹ ∨ b ∈ ↑(maxInvFreeSet X)}
⊢ a⁻¹ ∉ {b | b = x⁻¹ ∨ b ∈ ↑(maxInvFreeSet X)}
Tactic:
simp only [Set.mem_setOf_eq] at h
Proof state after:
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h✝ : x ∉ ↑(maxInvFreeSet X)
a : X
h : a = x⁻¹ ∨ a ∈ ↑(maxInvFreeSet X)
⊢ a⁻¹ ∉ {b | b = x⁻¹ ∨ b ∈ ↑(maxInvFreeSet X)}
Theorem: Classical.ProperInvolutiveInv.maxInvFreeSet_mem_inv
Proof state before:
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h✝ : x ∉ ↑(maxInvFreeSet X)
a : X
h : a = x⁻¹ ∨ a ∈ ↑(maxInvFreeSet X)
⊢ a⁻¹ ∉ {b | b = x⁻¹ ∨ b ∈ ↑(maxInvFreeSet X)}
Tactic:
cases h
Proof state after:
case inl
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h : x ∉ ↑(maxInvFreeSet X)
a : X
h✝ : a = x⁻¹
⊢ a⁻¹ ∉ {b | b = x⁻¹ ∨ b ∈ ↑(maxInvFreeSet X)}

case inr
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h : x ∉ ↑(maxInvFreeSet X)
a : X
h✝ : a ∈ ↑(maxInvFreeSet X)
⊢ a⁻¹ ∉ {b | b = x⁻¹ ∨ b ∈ ↑(maxInvFreeSet X)}
Theorem: Classical.ProperInvolutiveInv.maxInvFreeSet_mem_inv
Proof state before:
case inl
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h : x ∉ ↑(maxInvFreeSet X)
a : X
h✝ : a = x⁻¹
⊢ a⁻¹ ∉ {b | b = x⁻¹ ∨ b ∈ ↑(maxInvFreeSet X)}
Tactic:
subst ‹a = x⁻¹›
Proof state after:
case inl
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h : x ∉ ↑(maxInvFreeSet X)
⊢ x⁻¹⁻¹ ∉ {b | b = x⁻¹ ∨ b ∈ ↑(maxInvFreeSet X)}
Theorem: Classical.ProperInvolutiveInv.maxInvFreeSet_mem_inv
Proof state before:
case inl
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h : x ∉ ↑(maxInvFreeSet X)
⊢ x⁻¹⁻¹ ∉ {b | b = x⁻¹ ∨ b ∈ ↑(maxInvFreeSet X)}
Tactic:
rw [ProperInvolutiveInv.toInvolutiveInv.inv_inv]
Proof state after:
case inl
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h : x ∉ ↑(maxInvFreeSet X)
⊢ x ∉ {b | b = x⁻¹ ∨ b ∈ ↑(maxInvFreeSet X)}
Theorem: Classical.ProperInvolutiveInv.maxInvFreeSet_mem_inv
Proof state before:
case inl
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h : x ∉ ↑(maxInvFreeSet X)
⊢ x ∉ {b | b = x⁻¹ ∨ b ∈ ↑(maxInvFreeSet X)}
Tactic:
simp [not_or]
Proof state after:
case inl
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h : x ∉ ↑(maxInvFreeSet X)
⊢ ¬x = x⁻¹ ∧ x ∉ ↑(maxInvFreeSet X)
Theorem: Classical.ProperInvolutiveInv.maxInvFreeSet_mem_inv
Proof state before:
case inl
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h : x ∉ ↑(maxInvFreeSet X)
⊢ ¬x = x⁻¹ ∧ x ∉ ↑(maxInvFreeSet X)
Tactic:
refine' ⟨_, h⟩
Proof state after:
case inl
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h : x ∉ ↑(maxInvFreeSet X)
⊢ ¬x = x⁻¹
Theorem: Classical.ProperInvolutiveInv.maxInvFreeSet_mem_inv
Proof state before:
case inl
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h : x ∉ ↑(maxInvFreeSet X)
⊢ ¬x = x⁻¹
Tactic:
exact ProperInvolutiveInv.no_fixed_points _
Proof state after:
no goals
Theorem: Classical.ProperInvolutiveInv.maxInvFreeSet_mem_inv
Proof state before:
case inr
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h : x ∉ ↑(maxInvFreeSet X)
a : X
h✝ : a ∈ ↑(maxInvFreeSet X)
⊢ a⁻¹ ∉ {b | b = x⁻¹ ∨ b ∈ ↑(maxInvFreeSet X)}
Tactic:
simp [not_or]
Proof state after:
case inr
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h : x ∉ ↑(maxInvFreeSet X)
a : X
h✝ : a ∈ ↑(maxInvFreeSet X)
⊢ ¬a = x ∧ a⁻¹ ∉ ↑(maxInvFreeSet X)
Theorem: Classical.ProperInvolutiveInv.maxInvFreeSet_mem_inv
Proof state before:
case inr
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h : x ∉ ↑(maxInvFreeSet X)
a : X
h✝ : a ∈ ↑(maxInvFreeSet X)
⊢ ¬a = x ∧ a⁻¹ ∉ ↑(maxInvFreeSet X)
Tactic:
constructor
Proof state after:
case inr.left
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h : x ∉ ↑(maxInvFreeSet X)
a : X
h✝ : a ∈ ↑(maxInvFreeSet X)
⊢ ¬a = x

case inr.right
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h : x ∉ ↑(maxInvFreeSet X)
a : X
h✝ : a ∈ ↑(maxInvFreeSet X)
⊢ a⁻¹ ∉ ↑(maxInvFreeSet X)
Theorem: Classical.ProperInvolutiveInv.maxInvFreeSet_mem_inv
Proof state before:
case inr.left
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h : x ∉ ↑(maxInvFreeSet X)
a : X
h✝ : a ∈ ↑(maxInvFreeSet X)
⊢ ¬a = x
Tactic:
rintro rfl
Proof state after:
case inr.left
X : Type u_1
inst✝ : ProperInvolutiveInv X
a : X
h✝ : a ∈ ↑(maxInvFreeSet X)
h : a ∉ ↑(maxInvFreeSet X)
⊢ False
Theorem: Classical.ProperInvolutiveInv.maxInvFreeSet_mem_inv
Proof state before:
case inr.left
X : Type u_1
inst✝ : ProperInvolutiveInv X
a : X
h✝ : a ∈ ↑(maxInvFreeSet X)
h : a ∉ ↑(maxInvFreeSet X)
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: Classical.ProperInvolutiveInv.maxInvFreeSet_mem_inv
Proof state before:
case inr.right
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h : x ∉ ↑(maxInvFreeSet X)
a : X
h✝ : a ∈ ↑(maxInvFreeSet X)
⊢ a⁻¹ ∉ ↑(maxInvFreeSet X)
Tactic:
apply (maxInvFreeSet X).prop a ‹_›
Proof state after:
no goals
Theorem: Classical.ProperInvolutiveInv.maxInvFreeSet_mem_inv
Proof state before:
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h : x ∉ ↑(maxInvFreeSet X)
C : InvFreeSets X :=
  { val := Set.insert x⁻¹ ↑(maxInvFreeSet X), property := (_ : InvFreeSet (Set.insert x⁻¹ ↑(maxInvFreeSet X))) }
⊢ ↑(maxInvFreeSet X) ⊆ ↑C
Tactic:
show (maxInvFreeSet X).val ⊆ (maxInvFreeSet X).val.insert x⁻¹
Proof state after:
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h : x ∉ ↑(maxInvFreeSet X)
C : InvFreeSets X :=
  { val := Set.insert x⁻¹ ↑(maxInvFreeSet X), property := (_ : InvFreeSet (Set.insert x⁻¹ ↑(maxInvFreeSet X))) }
⊢ ↑(maxInvFreeSet X) ⊆ Set.insert x⁻¹ ↑(maxInvFreeSet X)
Theorem: Classical.ProperInvolutiveInv.maxInvFreeSet_mem_inv
Proof state before:
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h : x ∉ ↑(maxInvFreeSet X)
C : InvFreeSets X :=
  { val := Set.insert x⁻¹ ↑(maxInvFreeSet X), property := (_ : InvFreeSet (Set.insert x⁻¹ ↑(maxInvFreeSet X))) }
⊢ ↑(maxInvFreeSet X) ⊆ Set.insert x⁻¹ ↑(maxInvFreeSet X)
Tactic:
intro _
Proof state after:
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h : x ∉ ↑(maxInvFreeSet X)
C : InvFreeSets X :=
  { val := Set.insert x⁻¹ ↑(maxInvFreeSet X), property := (_ : InvFreeSet (Set.insert x⁻¹ ↑(maxInvFreeSet X))) }
a✝ : X
⊢ a✝ ∈ ↑(maxInvFreeSet X) → a✝ ∈ Set.insert x⁻¹ ↑(maxInvFreeSet X)
Theorem: Classical.ProperInvolutiveInv.maxInvFreeSet_mem_inv
Proof state before:
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h : x ∉ ↑(maxInvFreeSet X)
C : InvFreeSets X :=
  { val := Set.insert x⁻¹ ↑(maxInvFreeSet X), property := (_ : InvFreeSet (Set.insert x⁻¹ ↑(maxInvFreeSet X))) }
a✝ : X
⊢ a✝ ∈ ↑(maxInvFreeSet X) → a✝ ∈ Set.insert x⁻¹ ↑(maxInvFreeSet X)
Tactic:
aesop (add norm simp [Set.insert])
Proof state after:
no goals
Theorem: Classical.ProperInvolutiveInv.selection
Proof state before:
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
⊢ xor (orientation x) (orientation x⁻¹) = true
Tactic:
rw [@Bool.xor_iff_ne]
Proof state after:
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
⊢ orientation x ≠ orientation x⁻¹
Theorem: Classical.ProperInvolutiveInv.selection
Proof state before:
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
⊢ orientation x ≠ orientation x⁻¹
Tactic:
dsimp [orientation]
Proof state after:
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
⊢ ¬decide (x ∈ ↑(maxInvFreeSet X)) = decide (x⁻¹ ∈ ↑(maxInvFreeSet X))
Theorem: Classical.ProperInvolutiveInv.selection
Proof state before:
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
⊢ ¬decide (x ∈ ↑(maxInvFreeSet X)) = decide (x⁻¹ ∈ ↑(maxInvFreeSet X))
Tactic:
rw [@decide_eq_decide]
Proof state after:
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
⊢ ¬(x ∈ ↑(maxInvFreeSet X) ↔ x⁻¹ ∈ ↑(maxInvFreeSet X))
Theorem: Classical.ProperInvolutiveInv.selection
Proof state before:
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
⊢ ¬(x ∈ ↑(maxInvFreeSet X) ↔ x⁻¹ ∈ ↑(maxInvFreeSet X))
Tactic:
intro hmem
Proof state after:
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
hmem : x ∈ ↑(maxInvFreeSet X) ↔ x⁻¹ ∈ ↑(maxInvFreeSet X)
⊢ False
Theorem: Classical.ProperInvolutiveInv.selection
Proof state before:
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
hmem : x ∈ ↑(maxInvFreeSet X) ↔ x⁻¹ ∈ ↑(maxInvFreeSet X)
⊢ False
Tactic:
rw [@iff_eq_eq] at hmem
Proof state after:
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
hmem : (x ∈ ↑(maxInvFreeSet X)) = (x⁻¹ ∈ ↑(maxInvFreeSet X))
⊢ False
Theorem: Classical.ProperInvolutiveInv.selection
Proof state before:
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
hmem : (x ∈ ↑(maxInvFreeSet X)) = (x⁻¹ ∈ ↑(maxInvFreeSet X))
⊢ False
Tactic:
by_cases hx:x ∈ (maxInvFreeSet X).val
Proof state after:
case pos
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
hmem : (x ∈ ↑(maxInvFreeSet X)) = (x⁻¹ ∈ ↑(maxInvFreeSet X))
hx : x ∈ ↑(maxInvFreeSet X)
⊢ False

case neg
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
hmem : (x ∈ ↑(maxInvFreeSet X)) = (x⁻¹ ∈ ↑(maxInvFreeSet X))
hx : x ∉ ↑(maxInvFreeSet X)
⊢ False
Theorem: Classical.ProperInvolutiveInv.selection
Proof state before:
case pos
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
hmem : (x ∈ ↑(maxInvFreeSet X)) = (x⁻¹ ∈ ↑(maxInvFreeSet X))
hx : x ∈ ↑(maxInvFreeSet X)
⊢ False
Tactic:
exact (maxInvFreeSet X).prop x hx (hmem ▸ hx)
Proof state after:
no goals
Theorem: Classical.ProperInvolutiveInv.selection
Proof state before:
case neg
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
hmem : (x ∈ ↑(maxInvFreeSet X)) = (x⁻¹ ∈ ↑(maxInvFreeSet X))
hx : x ∉ ↑(maxInvFreeSet X)
⊢ False
Tactic:
have :=  maxInvFreeSet_mem_inv hx
Proof state after:
case neg
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
hmem : (x ∈ ↑(maxInvFreeSet X)) = (x⁻¹ ∈ ↑(maxInvFreeSet X))
hx : x ∉ ↑(maxInvFreeSet X)
this : x⁻¹ ∈ ↑(maxInvFreeSet X)
⊢ False
Theorem: Classical.ProperInvolutiveInv.selection
Proof state before:
case neg
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
hmem : (x ∈ ↑(maxInvFreeSet X)) = (x⁻¹ ∈ ↑(maxInvFreeSet X))
hx : x ∉ ↑(maxInvFreeSet X)
this : x⁻¹ ∈ ↑(maxInvFreeSet X)
⊢ False
Tactic:
rw [← hmem] at this
Proof state after:
case neg
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
hmem : (x ∈ ↑(maxInvFreeSet X)) = (x⁻¹ ∈ ↑(maxInvFreeSet X))
hx : x ∉ ↑(maxInvFreeSet X)
this : x ∈ ↑(maxInvFreeSet X)
⊢ False
Theorem: Classical.ProperInvolutiveInv.selection
Proof state before:
case neg
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
hmem : (x ∈ ↑(maxInvFreeSet X)) = (x⁻¹ ∈ ↑(maxInvFreeSet X))
hx : x ∉ ↑(maxInvFreeSet X)
this : x ∈ ↑(maxInvFreeSet X)
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: SymmFreeGroup.induced_restrict_eq_iff_lift_unique
Proof state before:
G : Type u_2
X : Type u_1
H : Type u_3
inst✝² : Group G
inst✝¹ : ProperInvolutiveInv X
inst✝ : Group H
ι : X →⁻¹ G
ind : {H : Type u_3} → [inst : Group H] → X →⁻¹ H → G →* H
⊢ (∀ (ψ : G →* H), ind (InvHom.comp ι (MonoidHom.toInvHom ψ)) = ψ) ↔
    ∀ (φ : X →⁻¹ H) (ψ : G →* H), InvHom.comp ι (MonoidHom.toInvHom ψ) = φ → ind φ = ψ
Tactic:
constructor
Proof state after:
case mp
G : Type u_2
X : Type u_1
H : Type u_3
inst✝² : Group G
inst✝¹ : ProperInvolutiveInv X
inst✝ : Group H
ι : X →⁻¹ G
ind : {H : Type u_3} → [inst : Group H] → X →⁻¹ H → G →* H
⊢ (∀ (ψ : G →* H), ind (InvHom.comp ι (MonoidHom.toInvHom ψ)) = ψ) →
    ∀ (φ : X →⁻¹ H) (ψ : G →* H), InvHom.comp ι (MonoidHom.toInvHom ψ) = φ → ind φ = ψ

case mpr
G : Type u_2
X : Type u_1
H : Type u_3
inst✝² : Group G
inst✝¹ : ProperInvolutiveInv X
inst✝ : Group H
ι : X →⁻¹ G
ind : {H : Type u_3} → [inst : Group H] → X →⁻¹ H → G →* H
⊢ (∀ (φ : X →⁻¹ H) (ψ : G →* H), InvHom.comp ι (MonoidHom.toInvHom ψ) = φ → ind φ = ψ) →
    ∀ (ψ : G →* H), ind (InvHom.comp ι (MonoidHom.toInvHom ψ)) = ψ
Theorem: SymmFreeGroup.induced_restrict_eq_iff_lift_unique
Proof state before:
case mp
G : Type u_2
X : Type u_1
H : Type u_3
inst✝² : Group G
inst✝¹ : ProperInvolutiveInv X
inst✝ : Group H
ι : X →⁻¹ G
ind : {H : Type u_3} → [inst : Group H] → X →⁻¹ H → G →* H
⊢ (∀ (ψ : G →* H), ind (InvHom.comp ι (MonoidHom.toInvHom ψ)) = ψ) →
    ∀ (φ : X →⁻¹ H) (ψ : G →* H), InvHom.comp ι (MonoidHom.toInvHom ψ) = φ → ind φ = ψ
Tactic:
intro h φ ψ hres
Proof state after:
case mp
G : Type u_2
X : Type u_1
H : Type u_3
inst✝² : Group G
inst✝¹ : ProperInvolutiveInv X
inst✝ : Group H
ι : X →⁻¹ G
ind : {H : Type u_3} → [inst : Group H] → X →⁻¹ H → G →* H
h : ∀ (ψ : G →* H), ind (InvHom.comp ι (MonoidHom.toInvHom ψ)) = ψ
φ : X →⁻¹ H
ψ : G →* H
hres : InvHom.comp ι (MonoidHom.toInvHom ψ) = φ
⊢ ind φ = ψ
Theorem: SymmFreeGroup.induced_restrict_eq_iff_lift_unique
Proof state before:
case mp
G : Type u_2
X : Type u_1
H : Type u_3
inst✝² : Group G
inst✝¹ : ProperInvolutiveInv X
inst✝ : Group H
ι : X →⁻¹ G
ind : {H : Type u_3} → [inst : Group H] → X →⁻¹ H → G →* H
h : ∀ (ψ : G →* H), ind (InvHom.comp ι (MonoidHom.toInvHom ψ)) = ψ
φ : X →⁻¹ H
ψ : G →* H
hres : InvHom.comp ι (MonoidHom.toInvHom ψ) = φ
⊢ ind φ = ψ
Tactic:
exact hres ▸ (h ψ)
Proof state after:
no goals
Theorem: SymmFreeGroup.induced_restrict_eq_iff_lift_unique
Proof state before:
case mpr
G : Type u_2
X : Type u_1
H : Type u_3
inst✝² : Group G
inst✝¹ : ProperInvolutiveInv X
inst✝ : Group H
ι : X →⁻¹ G
ind : {H : Type u_3} → [inst : Group H] → X →⁻¹ H → G →* H
⊢ (∀ (φ : X →⁻¹ H) (ψ : G →* H), InvHom.comp ι (MonoidHom.toInvHom ψ) = φ → ind φ = ψ) →
    ∀ (ψ : G →* H), ind (InvHom.comp ι (MonoidHom.toInvHom ψ)) = ψ
Tactic:
intro h ψ
Proof state after:
case mpr
G : Type u_2
X : Type u_1
H : Type u_3
inst✝² : Group G
inst✝¹ : ProperInvolutiveInv X
inst✝ : Group H
ι : X →⁻¹ G
ind : {H : Type u_3} → [inst : Group H] → X →⁻¹ H → G →* H
h : ∀ (φ : X →⁻¹ H) (ψ : G →* H), InvHom.comp ι (MonoidHom.toInvHom ψ) = φ → ind φ = ψ
ψ : G →* H
⊢ ind (InvHom.comp ι (MonoidHom.toInvHom ψ)) = ψ
Theorem: SymmFreeGroup.induced_restrict_eq_iff_lift_unique
Proof state before:
case mpr
G : Type u_2
X : Type u_1
H : Type u_3
inst✝² : Group G
inst✝¹ : ProperInvolutiveInv X
inst✝ : Group H
ι : X →⁻¹ G
ind : {H : Type u_3} → [inst : Group H] → X →⁻¹ H → G →* H
h : ∀ (φ : X →⁻¹ H) (ψ : G →* H), InvHom.comp ι (MonoidHom.toInvHom ψ) = φ → ind φ = ψ
ψ : G →* H
⊢ ind (InvHom.comp ι (MonoidHom.toInvHom ψ)) = ψ
Tactic:
exact h (ι.comp ψ.toInvHom) ψ rfl
Proof state after:
no goals
Theorem: cantor_diagonal'
Proof state before:
α : Type
f : α → α → Bool
⊢ ∃ t, ∀ (a : α), t ≠ f a
Tactic:
apply Exists.intro (fun a ↦ !(f a a) )
Proof state after:
α : Type
f : α → α → Bool
⊢ ∀ (a : α), (fun a => !f a a) ≠ f a
Theorem: cantor_diagonal'
Proof state before:
α : Type
f : α → α → Bool
⊢ ∀ (a : α), (fun a => !f a a) ≠ f a
Tactic:
intro a h
Proof state after:
α : Type
f : α → α → Bool
a : α
h : (fun a => !f a a) = f a
⊢ False
Theorem: cantor_diagonal'
Proof state before:
α : Type
f : α → α → Bool
a : α
h : (fun a => !f a a) = f a
⊢ False
Tactic:
let h' := congrFun h a
Proof state after:
α : Type
f : α → α → Bool
a : α
h : (fun a => !f a a) = f a
h' : (!f a a) = f a a := congrFun h a
⊢ False
Theorem: cantor_diagonal'
Proof state before:
α : Type
f : α → α → Bool
a : α
h : (fun a => !f a a) = f a
h' : (!f a a) = f a a := congrFun h a
⊢ False
Tactic:
by_cases c:f a a <;> simp [c] at h'
Proof state after:
no goals
Theorem: Graph.redCons_nil
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v : V
e : EdgeBetween G u v
⊢ redCons e (nil v) = cons e (nil v)
Tactic:
simp [redCons]
Proof state after:
no goals
Theorem: Graph.redCons_cons_vertex_neq
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v v' w : V
e : EdgeBetween G u v
e' : EdgeBetween G v v'
p : EdgePath G v' w
h : v' ≠ u
⊢ redCons e (cons e' p) = cons e (cons e' p)
Tactic:
simp [redCons, h]
Proof state after:
no goals
Theorem: Graph.redCons_cons_edge_neq
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v w : V
e : EdgeBetween G u v
e' : EdgeBetween G v u
p : EdgePath G u w
h : e' ≠ EdgeBetween.bar e
⊢ redCons e (cons e' p) = cons e (cons e' p)
Tactic:
simp [redCons, h]
Proof state after:
no goals
Theorem: Graph.redCons_cons_edge_eq
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v w : V
e : EdgeBetween G u v
e' : EdgeBetween G v u
p : EdgePath G u w
h : e' = EdgeBetween.bar e
⊢ redCons e (cons e' p) = p
Tactic:
simp [redCons, h]
Proof state after:
no goals
Theorem: Graph.prepend_cases
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v w : V
e : EdgeBetween G u v
p : EdgePath G v w
⊢ redCons e p = cons e p ∨ ∃ t, p = cons (EdgeBetween.bar e) t ∧ redCons e p = t
Tactic:
match p with
| nil _ =>
  simp only [redCons_nil, false_and, exists_false, or_false]
| cons e' p' =>
  rename_i w' w''
  if c:w'' = u then
    cases c
    if c':e' = e.bar
      then
        simp [redCons_cons_edge_eq p' c']
        simp only [c', or_true]
      else
        simp [redCons_cons_edge_neq p' c']
  else
    simp only [redCons_cons_vertex_neq e e' p' c, cons.injEq, exists_eq_right', true_or]
Proof state after:
no goals
Theorem: Graph.prepend_cases
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v w : V
e : EdgeBetween G u v
p : EdgePath G v w
⊢ redCons e (nil v) = cons e (nil v) ∨ ∃ t, nil v = cons (EdgeBetween.bar e) t ∧ redCons e (nil v) = t
Tactic:
simp only [redCons_nil, false_and, exists_false, or_false]
Proof state after:
no goals