Theorem: Classical.InvFreeSets.chains_bounded_above (GroupComp/SymmFreeGroup.lean)

State before:
X : Type u_1
inst✝ : ProperInvolutiveInv X
c : Set (InvFreeSets X)
hcChain : IsChain LE.le c
⊢ BddAbove c
Tactic:
dsimp [BddAbove, upperBounds]
State after:
X : Type u_1
inst✝ : ProperInvolutiveInv X
c : Set (InvFreeSets X)
hcChain : IsChain LE.le c
⊢ Set.Nonempty {x | ∀ ⦃a : InvFreeSets X⦄, a ∈ c → a ≤ x}

State before:
X : Type u_1
inst✝ : ProperInvolutiveInv X
c : Set (InvFreeSets X)
hcChain : IsChain LE.le c
⊢ Set.Nonempty {x | ∀ ⦃a : InvFreeSets X⦄, a ∈ c → a ≤ x}
Tactic:
let sup := InvFreeSets.chainUnion c hcChain
State after:
X : Type u_1
inst✝ : ProperInvolutiveInv X
c : Set (InvFreeSets X)
hcChain : IsChain LE.le c
sup : InvFreeSets X := chainUnion c hcChain
⊢ Set.Nonempty {x | ∀ ⦃a : InvFreeSets X⦄, a ∈ c → a ≤ x}

State before:
X : Type u_1
inst✝ : ProperInvolutiveInv X
c : Set (InvFreeSets X)
hcChain : IsChain LE.le c
sup : InvFreeSets X := chainUnion c hcChain
⊢ Set.Nonempty {x | ∀ ⦃a : InvFreeSets X⦄, a ∈ c → a ≤ x}
Tactic:
use sup
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
⊢ sup ∈ {x | ∀ ⦃a : InvFreeSets X⦄, a ∈ c → a ≤ x}

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
⊢ sup ∈ {x | ∀ ⦃a : InvFreeSets X⦄, a ∈ c → a ≤ x}
Tactic:
intro A hAc
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
⊢ A ≤ sup

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
⊢ A ≤ sup
Tactic:
simp only [LE.le, chainUnion, Monad.join, joinM, Set.bind_def, Set.mem_image, exists_and_right,
  exists_eq_right, id_eq, Set.iUnion_exists]
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
⊢ Set.Subset (↑A) (⋃ i, ⋃ i_1, ⋃ (_ : i_1 ∈ c ∧ ↑i_1 = i), i)

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
⊢ Set.Subset (↑A) (⋃ i, ⋃ i_1, ⋃ (_ : i_1 ∈ c ∧ ↑i_1 = i), i)
Tactic:
intro x hxA
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
⊢ x ∈ ⋃ i, ⋃ i_1, ⋃ (_ : i_1 ∈ c ∧ ↑i_1 = i), i

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
⊢ x ∈ ⋃ i, ⋃ i_1, ⋃ (_ : i_1 ∈ c ∧ ↑i_1 = i), i
Tactic:
use A
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
⊢ (↑A ∈ Set.range fun i => ⋃ i_1, ⋃ (_ : i_1 ∈ c ∧ ↑i_1 = i), i) ∧ x ∈ ↑A

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) ∧ x ∈ ↑A
Tactic:
refine' ⟨_, hxA⟩
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
⊢ ↑A ∈ Set.range fun i => ⋃ i_1, ⋃ (_ : i_1 ∈ c ∧ ↑i_1 = i), i

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

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

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

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

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

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