Theorem: Classical.ProperInvolutiveInv.maxInvFreeSet_mem_inv (GroupComp/SymmFreeGroup.lean)

State before:
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
⊢ x ∉ ↑(maxInvFreeSet X) → x⁻¹ ∈ ↑(maxInvFreeSet X)
Tactic:
intro h
State after:
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h : x ∉ ↑(maxInvFreeSet X)
⊢ x⁻¹ ∈ ↑(maxInvFreeSet X)

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])
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)

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
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)

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]
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

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]
State after:
no goals

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]
State after:
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h : x ∉ ↑(maxInvFreeSet X)
⊢ InvFreeSet {b | b = x⁻¹ ∨ b ∈ ↑(maxInvFreeSet X)}

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
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)}

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
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)}

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
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)}

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⁻¹›
State after:
case inl
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h : x ∉ ↑(maxInvFreeSet X)
⊢ x⁻¹⁻¹ ∉ {b | b = x⁻¹ ∨ b ∈ ↑(maxInvFreeSet X)}

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]
State after:
case inl
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h : x ∉ ↑(maxInvFreeSet X)
⊢ x ∉ {b | b = x⁻¹ ∨ b ∈ ↑(maxInvFreeSet X)}

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]
State after:
case inl
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h : x ∉ ↑(maxInvFreeSet X)
⊢ ¬x = x⁻¹ ∧ x ∉ ↑(maxInvFreeSet X)

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⟩
State after:
case inl
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h : x ∉ ↑(maxInvFreeSet X)
⊢ ¬x = x⁻¹

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 _
State after:
no goals

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]
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)

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
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)

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
State after:
case inr.left
X : Type u_1
inst✝ : ProperInvolutiveInv X
a : X
h✝ : a ∈ ↑(maxInvFreeSet X)
h : a ∉ ↑(maxInvFreeSet X)
⊢ False

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
State after:
no goals

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 ‹_›
State after:
no goals

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⁻¹
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)

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 _
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)

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])
State after:
no goals