ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
this :
  ↑FreeGroup.lift a =
    MonoidHom.comp (↑lift fun i => ↑FreeGroup.lift fun x => a i) (MulEquiv.toMonoidHom freeGroupEquivFreeProduct)
⊢ Function.Injective ↑(↑FreeGroup.lift a)
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
⊢ Function.Injective ↑(↑FreeGroup.lift a)
have : FreeGroup.lift a =
    (FreeProduct.lift fun i => FreeGroup.lift fun _ => a i).comp
      (@freeGroupEquivFreeProduct ι).toMonoidHom := by
  ext i
  simp
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
this :
  ↑FreeGroup.lift a =
    MonoidHom.comp (↑lift fun i => ↑FreeGroup.lift fun x => a i) (MulEquiv.toMonoidHom freeGroupEquivFreeProduct)
⊢ Function.Injective
    (↑(↑lift fun i => ↑FreeGroup.lift fun x => a i) ∘ ↑(MulEquiv.toMonoidHom freeGroupEquivFreeProduct))
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
this :
  ↑FreeGroup.lift a =
    MonoidHom.comp (↑lift fun i => ↑FreeGroup.lift fun x => a i) (MulEquiv.toMonoidHom freeGroupEquivFreeProduct)
⊢ Function.Injective ↑(↑FreeGroup.lift a)
rw [this, MonoidHom.coe_comp]
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
⊢ Function.Injective
    (↑(↑lift fun i => ↑FreeGroup.lift fun x => a i) ∘ ↑(MulEquiv.toMonoidHom freeGroupEquivFreeProduct))
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
this :
  ↑FreeGroup.lift a =
    MonoidHom.comp (↑lift fun i => ↑FreeGroup.lift fun x => a i) (MulEquiv.toMonoidHom freeGroupEquivFreeProduct)
⊢ Function.Injective
    (↑(↑lift fun i => ↑FreeGroup.lift fun x => a i) ∘ ↑(MulEquiv.toMonoidHom freeGroupEquivFreeProduct))
clear this
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
⊢ Function.Injective ↑(↑lift fun i => ↑FreeGroup.lift fun x => a i)
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
⊢ Function.Injective
    (↑(↑lift fun i => ↑FreeGroup.lift fun x => a i) ∘ ↑(MulEquiv.toMonoidHom freeGroupEquivFreeProduct))
refine' Function.Injective.comp _ (MulEquiv.injective freeGroupEquivFreeProduct)
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
⊢ Function.Injective ↑(↑lift fun i => ↑FreeGroup.lift fun x => a i)
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
⊢ Function.Injective ↑(↑lift fun i => ↑FreeGroup.lift fun x => a i)
show Function.Injective (lift fun i : ι => FreeGroup.lift fun _ => a i)
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
⊢ Function.Injective ↑(↑lift fun i => ↑FreeGroup.lift fun x => a i)
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
⊢ Function.Injective ↑(↑lift fun i => ↑FreeGroup.lift fun x => a i)
let H : ι → Type _ := fun _i => FreeGroup Unit
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
⊢ Function.Injective ↑(↑lift fun i => ↑FreeGroup.lift fun x => a i)
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
⊢ Function.Injective ↑(↑lift fun i => ↑FreeGroup.lift fun x => a i)
let f : ∀ i, H i →* G := fun i => FreeGroup.lift fun _ => a i
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
⊢ Function.Injective ↑(↑lift fun i => ↑FreeGroup.lift fun x => a i)
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
⊢ Function.Injective ↑(↑lift fun i => ↑FreeGroup.lift fun x => a i)
let X' : ι → Set α := fun i => X i ∪ Y i
case hXnonempty
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
⊢ ∀ (i : ι), Set.Nonempty (X' i)

case hXdisj
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
⊢ Pairwise fun i j => Disjoint (X' i) (X' j)

case hpp
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
⊢ Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X' j ⊆ X' i

ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
⊢ 3 ≤ (#ι) ∨ ∃ i, 3 ≤ (#H i)
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
⊢ Function.Injective ↑(↑lift fun i => ↑FreeGroup.lift fun x => a i)
apply lift_injective_of_ping_pong f _ X'
case hXnonempty
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
⊢ ∀ (i : ι), Set.Nonempty (X' i)

case hXdisj
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
⊢ Pairwise fun i j => Disjoint (X' i) (X' j)

case hpp
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
⊢ Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X' j ⊆ X' i

ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
⊢ 3 ≤ (#ι) ∨ ∃ i, 3 ≤ (#H i)
case hXnonempty
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
⊢ ∀ (i : ι), Set.Nonempty (X' i)

case hXdisj
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
⊢ Pairwise fun i j => Disjoint (X' i) (X' j)

case hpp
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
⊢ Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X' j ⊆ X' i

ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
⊢ 3 ≤ (#ι) ∨ ∃ i, 3 ≤ (#H i)
show ∀ i, (X' i).Nonempty
case hXdisj
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
⊢ Pairwise fun i j => Disjoint (X' i) (X' j)

case hpp
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
⊢ Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X' j ⊆ X' i

ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
⊢ 3 ≤ (#ι) ∨ ∃ i, 3 ≤ (#H i)
case hXdisj
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
⊢ Pairwise fun i j => Disjoint (X' i) (X' j)

case hpp
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
⊢ Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X' j ⊆ X' i

ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
⊢ 3 ≤ (#ι) ∨ ∃ i, 3 ≤ (#H i)
show Pairwise fun i j => Disjoint (X' i) (X' j)
case hpp
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
⊢ Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X' j ⊆ X' i

ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
⊢ 3 ≤ (#ι) ∨ ∃ i, 3 ≤ (#H i)
case hpp
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
⊢ Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X' j ⊆ X' i

ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
⊢ 3 ≤ (#ι) ∨ ∃ i, 3 ≤ (#H i)
show Pairwise fun i j => ∀ h : H i, h ≠ 1 → f i h • X' j ⊆ X' i
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
⊢ 3 ≤ (#ι) ∨ ∃ i, 3 ≤ (#H i)
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
⊢ 3 ≤ (#ι) ∨ ∃ i, 3 ≤ (#H i)
show _ ∨ ∃ i, 3 ≤ (#H i)
case h
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
i : IsFreeGroup.Generators (FreeGroup ι)
⊢ ↑(↑FreeGroup.lift a) (IsFreeGroup.of i) =
    ↑(MonoidHom.comp (↑lift fun i => ↑FreeGroup.lift fun x => a i) (MulEquiv.toMonoidHom freeGroupEquivFreeProduct))
      (IsFreeGroup.of i)
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
⊢ ↑FreeGroup.lift a =
    MonoidHom.comp (↑lift fun i => ↑FreeGroup.lift fun x => a i) (MulEquiv.toMonoidHom freeGroupEquivFreeProduct)
ext i
no goals
case h
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
i : IsFreeGroup.Generators (FreeGroup ι)
⊢ ↑(↑FreeGroup.lift a) (IsFreeGroup.of i) =
    ↑(MonoidHom.comp (↑lift fun i => ↑FreeGroup.lift fun x => a i) (MulEquiv.toMonoidHom freeGroupEquivFreeProduct))
      (IsFreeGroup.of i)
simp
no goals
case hXnonempty
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
⊢ ∀ (i : ι), Set.Nonempty (X' i)
exact fun i => Set.Nonempty.inl (hXnonempty i)
case hXdisj
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
⊢ Disjoint (X' i) (X' j)
case hXdisj
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
⊢ Pairwise fun i j => Disjoint (X' i) (X' j)
intro i j hij
case hXdisj
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
⊢ Disjoint (X i ∪ Y i) (X j ∪ Y j)
case hXdisj
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
⊢ Disjoint (X' i) (X' j)
simp only
case hXdisj.hs.ht
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
⊢ Disjoint (X i) (X j)

case hXdisj.hs.hu
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
⊢ Disjoint (X i) (Y j)

case hXdisj.ht.ht
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
⊢ Disjoint (Y i) (X j)

case hXdisj.ht.hu
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
⊢ Disjoint (Y i) (Y j)
case hXdisj
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
⊢ Disjoint (X i ∪ Y i) (X j ∪ Y j)
apply Disjoint.union_left <;> apply Disjoint.union_right
no goals
case hXdisj.hs.ht
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
⊢ Disjoint (X i) (X j)
exact hXdisj hij
no goals
case hXdisj.hs.hu
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
⊢ Disjoint (X i) (Y j)
exact hXYdisj i j
no goals
case hXdisj.ht.ht
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
⊢ Disjoint (Y i) (X j)
exact (hXYdisj j i).symm
no goals
case hXdisj.ht.hu
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
⊢ Disjoint (Y i) (Y j)
exact hYdisj hij
case hpp
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
⊢ ∀ (h : H i), h ≠ 1 → ↑(f i) h • X' j ⊆ X' i
case hpp
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
⊢ Pairwise fun i j => ∀ (h : H i), h ≠ 1 → ↑(f i) h • X' j ⊆ X' i
rintro i j hij
case hpp
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
⊢ ∀ (y : ℤ),
    ↑FreeGroup.freeGroupUnitEquivInt.symm y ≠ 1 → ↑(f i) (↑FreeGroup.freeGroupUnitEquivInt.symm y) • X' j ⊆ X' i
case hpp
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
⊢ ∀ (h : H i), h ≠ 1 → ↑(f i) h • X' j ⊆ X' i
refine' FreeGroup.freeGroupUnitEquivInt.forall_congr_left'.mpr _
case hpp
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hne1 : ↑FreeGroup.freeGroupUnitEquivInt.symm n ≠ 1
⊢ ↑(f i) (↑FreeGroup.freeGroupUnitEquivInt.symm n) • X' j ⊆ X' i
case hpp
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
⊢ ∀ (y : ℤ),
    ↑FreeGroup.freeGroupUnitEquivInt.symm y ≠ 1 → ↑(f i) (↑FreeGroup.freeGroupUnitEquivInt.symm y) • X' j ⊆ X' i
intro n hne1
case hpp
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hne1 : ↑FreeGroup.freeGroupUnitEquivInt.symm n ≠ 1
⊢ ↑(↑FreeGroup.lift fun x => a i) (FreeGroup.of () ^ n) • X' j ⊆ X' i
case hpp
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hne1 : ↑FreeGroup.freeGroupUnitEquivInt.symm n ≠ 1
⊢ ↑(f i) (↑FreeGroup.freeGroupUnitEquivInt.symm n) • X' j ⊆ X' i
change FreeGroup.lift (fun _ => a i) (FreeGroup.of () ^ n) • X' j ⊆ X' i
case hpp
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hne1 : ↑FreeGroup.freeGroupUnitEquivInt.symm n ≠ 1
⊢ a i ^ n • (X j ∪ Y j) ⊆ X i ∪ Y i
case hpp
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hne1 : ↑FreeGroup.freeGroupUnitEquivInt.symm n ≠ 1
⊢ ↑(↑FreeGroup.lift fun x => a i) (FreeGroup.of () ^ n) • X' j ⊆ X' i
simp only [map_zpow, FreeGroup.lift.of]
case hpp
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hne1 : ↑FreeGroup.freeGroupUnitEquivInt.symm n ≠ 1
⊢ a i ^ n • X' j ⊆ X' i
case hpp
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hne1 : ↑FreeGroup.freeGroupUnitEquivInt.symm n ≠ 1
⊢ a i ^ n • (X j ∪ Y j) ⊆ X i ∪ Y i
change a i ^ n • X' j ⊆ X' i
case hpp
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hne1 : ↑FreeGroup.freeGroupUnitEquivInt.symm n ≠ 1
hnne0 : n ≠ 0
⊢ a i ^ n • X' j ⊆ X' i
case hpp
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hne1 : ↑FreeGroup.freeGroupUnitEquivInt.symm n ≠ 1
⊢ a i ^ n • X' j ⊆ X' i
have hnne0 : n ≠ 0 := by
  rintro rfl
  apply hne1
  simp; rfl
case hpp
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hnne0 : n ≠ 0
⊢ a i ^ n • X' j ⊆ X' i
case hpp
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hne1 : ↑FreeGroup.freeGroupUnitEquivInt.symm n ≠ 1
hnne0 : n ≠ 0
⊢ a i ^ n • X' j ⊆ X' i
clear hne1
case hpp
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hnne0 : n ≠ 0
⊢ a i ^ n • (X j ∪ Y j) ⊆ X i ∪ Y i
case hpp
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hnne0 : n ≠ 0
⊢ a i ^ n • X' j ⊆ X' i
simp only
case hpp.inl
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hnne0 : n ≠ 0
hlt : n > 0
⊢ a i ^ n • (X j ∪ Y j) ⊆ X i ∪ Y i

case hpp.inr
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hnne0 : n ≠ 0
hgt : n < 0
⊢ a i ^ n • (X j ∪ Y j) ⊆ X i ∪ Y i
case hpp
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hnne0 : n ≠ 0
⊢ a i ^ n • (X j ∪ Y j) ⊆ X i ∪ Y i
cases' (lt_or_gt_of_ne hnne0).symm with hlt hgt
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
hne1 : ↑FreeGroup.freeGroupUnitEquivInt.symm 0 ≠ 1
⊢ False
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hne1 : ↑FreeGroup.freeGroupUnitEquivInt.symm n ≠ 1
⊢ n ≠ 0
rintro rfl
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
hne1 : ↑FreeGroup.freeGroupUnitEquivInt.symm 0 ≠ 1
⊢ ↑FreeGroup.freeGroupUnitEquivInt.symm 0 = 1
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
hne1 : ↑FreeGroup.freeGroupUnitEquivInt.symm 0 ≠ 1
⊢ False
apply hne1
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
hne1 : ↑FreeGroup.freeGroupUnitEquivInt.symm 0 ≠ 1
⊢ ↑FreeGroup.freeGroupUnitEquivInt.symm 0 = 1
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
hne1 : ↑FreeGroup.freeGroupUnitEquivInt.symm 0 ≠ 1
⊢ ↑FreeGroup.freeGroupUnitEquivInt.symm 0 = 1
simp
no goals
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
hne1 : ↑FreeGroup.freeGroupUnitEquivInt.symm 0 ≠ 1
⊢ ↑FreeGroup.freeGroupUnitEquivInt.symm 0 = 1
rfl
case hpp.inl
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hnne0 : n ≠ 0
hlt : n > 0
h1n : 1 ≤ n
⊢ a i ^ n • (X j ∪ Y j) ⊆ X i ∪ Y i
case hpp.inl
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hnne0 : n ≠ 0
hlt : n > 0
⊢ a i ^ n • (X j ∪ Y j) ⊆ X i ∪ Y i
have h1n : 1 ≤ n := hlt
no goals
case hpp.inl
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hnne0 : n ≠ 0
hlt : n > 0
h1n : 1 ≤ n
⊢ a i ^ n • (X j ∪ Y j) ⊆ X i ∪ Y i
calc
  a i ^ n • X' j ⊆ a i ^ n • Y iᶜ :=
    smul_set_mono ((hXYdisj j i).union_left <| hYdisj hij.symm).subset_compl_right
  _ ⊆ X i := by
    clear hnne0 hlt
    refine Int.le_induction (P := fun n => a i ^ n • Y iᶜ ⊆ X i) ?_ ?_ n h1n
    . dsimp
      rw [zpow_one]
      exact hX i
    . dsimp
      intro n _hle hi
      calc
        a i ^ (n + 1) • Y iᶜ = (a i ^ n * a i) • Y iᶜ := by rw [zpow_add, zpow_one]
        _ = a i ^ n • a i • Y iᶜ := (MulAction.mul_smul _ _ _)
        _ ⊆ a i ^ n • X i := (smul_set_mono <| hX i)
        _ ⊆ a i ^ n • Y iᶜ := (smul_set_mono (hXYdisj i i).subset_compl_right)
        _ ⊆ X i := hi
  _ ⊆ X' i := Set.subset_union_left _ _
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
h1n : 1 ≤ n
⊢ a i ^ n • Y iᶜ ⊆ X i
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hnne0 : n ≠ 0
hlt : n > 0
h1n : 1 ≤ n
⊢ a i ^ n • Y iᶜ ⊆ X i
clear hnne0 hlt
case refine_1
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
h1n : 1 ≤ n
⊢ (fun n => a i ^ n • Y iᶜ ⊆ X i) 1

case refine_2
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
h1n : 1 ≤ n
⊢ ∀ (n : ℤ), 1 ≤ n → (fun n => a i ^ n • Y iᶜ ⊆ X i) n → (fun n => a i ^ n • Y iᶜ ⊆ X i) (n + 1)
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
h1n : 1 ≤ n
⊢ a i ^ n • Y iᶜ ⊆ X i
refine Int.le_induction (P := fun n => a i ^ n • Y iᶜ ⊆ X i) ?_ ?_ n h1n
case refine_2
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
h1n : 1 ≤ n
⊢ ∀ (n : ℤ), 1 ≤ n → (fun n => a i ^ n • Y iᶜ ⊆ X i) n → (fun n => a i ^ n • Y iᶜ ⊆ X i) (n + 1)
case refine_1
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
h1n : 1 ≤ n
⊢ (fun n => a i ^ n • Y iᶜ ⊆ X i) 1

case refine_2
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
h1n : 1 ≤ n
⊢ ∀ (n : ℤ), 1 ≤ n → (fun n => a i ^ n • Y iᶜ ⊆ X i) n → (fun n => a i ^ n • Y iᶜ ⊆ X i) (n + 1)
. dsimp
  rw [zpow_one]
  exact hX i
no goals
case refine_2
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
h1n : 1 ≤ n
⊢ ∀ (n : ℤ), 1 ≤ n → (fun n => a i ^ n • Y iᶜ ⊆ X i) n → (fun n => a i ^ n • Y iᶜ ⊆ X i) (n + 1)
. dsimp
  intro n _hle hi
  calc
    a i ^ (n + 1) • Y iᶜ = (a i ^ n * a i) • Y iᶜ := by rw [zpow_add, zpow_one]
    _ = a i ^ n • a i • Y iᶜ := (MulAction.mul_smul _ _ _)
    _ ⊆ a i ^ n • X i := (smul_set_mono <| hX i)
    _ ⊆ a i ^ n • Y iᶜ := (smul_set_mono (hXYdisj i i).subset_compl_right)
    _ ⊆ X i := hi
case refine_1
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
h1n : 1 ≤ n
⊢ a i ^ 1 • Y iᶜ ⊆ X i
case refine_1
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
h1n : 1 ≤ n
⊢ (fun n => a i ^ n • Y iᶜ ⊆ X i) 1
dsimp
case refine_1
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
h1n : 1 ≤ n
⊢ a i • Y iᶜ ⊆ X i
case refine_1
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
h1n : 1 ≤ n
⊢ a i ^ 1 • Y iᶜ ⊆ X i
rw [zpow_one]
no goals
case refine_1
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
h1n : 1 ≤ n
⊢ a i • Y iᶜ ⊆ X i
exact hX i
case refine_2
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
h1n : 1 ≤ n
⊢ ∀ (n : ℤ), 1 ≤ n → a i ^ n • Y iᶜ ⊆ X i → a i ^ (n + 1) • Y iᶜ ⊆ X i
case refine_2
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
h1n : 1 ≤ n
⊢ ∀ (n : ℤ), 1 ≤ n → (fun n => a i ^ n • Y iᶜ ⊆ X i) n → (fun n => a i ^ n • Y iᶜ ⊆ X i) (n + 1)
dsimp
case refine_2
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n✝ : ℤ
h1n : 1 ≤ n✝
n : ℤ
_hle : 1 ≤ n
hi : a i ^ n • Y iᶜ ⊆ X i
⊢ a i ^ (n + 1) • Y iᶜ ⊆ X i
case refine_2
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
h1n : 1 ≤ n
⊢ ∀ (n : ℤ), 1 ≤ n → a i ^ n • Y iᶜ ⊆ X i → a i ^ (n + 1) • Y iᶜ ⊆ X i
intro n _hle hi
no goals
case refine_2
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n✝ : ℤ
h1n : 1 ≤ n✝
n : ℤ
_hle : 1 ≤ n
hi : a i ^ n • Y iᶜ ⊆ X i
⊢ a i ^ (n + 1) • Y iᶜ ⊆ X i
calc
  a i ^ (n + 1) • Y iᶜ = (a i ^ n * a i) • Y iᶜ := by rw [zpow_add, zpow_one]
  _ = a i ^ n • a i • Y iᶜ := (MulAction.mul_smul _ _ _)
  _ ⊆ a i ^ n • X i := (smul_set_mono <| hX i)
  _ ⊆ a i ^ n • Y iᶜ := (smul_set_mono (hXYdisj i i).subset_compl_right)
  _ ⊆ X i := hi
no goals
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n✝ : ℤ
h1n : 1 ≤ n✝
n : ℤ
_hle : 1 ≤ n
hi : a i ^ n • Y iᶜ ⊆ X i
⊢ a i ^ (n + 1) • Y iᶜ = (a i ^ n * a i) • Y iᶜ
rw [zpow_add, zpow_one]
case hpp.inr
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hnne0 : n ≠ 0
hgt : n < 0
h1n : n ≤ -1
⊢ a i ^ n • (X j ∪ Y j) ⊆ X i ∪ Y i
case hpp.inr
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hnne0 : n ≠ 0
hgt : n < 0
⊢ a i ^ n • (X j ∪ Y j) ⊆ X i ∪ Y i
have h1n : n ≤ -1 := by
  apply Int.le_of_lt_add_one
  simpa using hgt
case H
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hnne0 : n ≠ 0
hgt : n < 0
⊢ n < -1 + 1
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hnne0 : n ≠ 0
hgt : n < 0
⊢ n ≤ -1
apply Int.le_of_lt_add_one
no goals
case H
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hnne0 : n ≠ 0
hgt : n < 0
⊢ n < -1 + 1
simpa using hgt
case refine'_1
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hnne0 : n ≠ 0
hgt : n < 0
h1n : n ≤ -1
⊢ (fun n => a i ^ n • X iᶜ ⊆ Y i) (-1)

case refine'_2
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hnne0 : n ≠ 0
hgt : n < 0
h1n : n ≤ -1
⊢ ∀ (n : ℤ), n ≤ -1 → (fun n => a i ^ n • X iᶜ ⊆ Y i) n → (fun n => a i ^ n • X iᶜ ⊆ Y i) (n - 1)
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hnne0 : n ≠ 0
hgt : n < 0
h1n : n ≤ -1
⊢ a i ^ n • X iᶜ ⊆ Y i
refine' Int.le_induction_down (P := fun n => a i ^ n • X iᶜ ⊆ Y i) _ _ _ h1n
case refine'_1
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hnne0 : n ≠ 0
hgt : n < 0
h1n : n ≤ -1
⊢ a i ^ (-1) • X iᶜ ⊆ Y i
case refine'_1
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hnne0 : n ≠ 0
hgt : n < 0
h1n : n ≤ -1
⊢ (fun n => a i ^ n • X iᶜ ⊆ Y i) (-1)
dsimp
case refine'_1
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hnne0 : n ≠ 0
hgt : n < 0
h1n : n ≤ -1
⊢ (a i)⁻¹ • X iᶜ ⊆ Y i
case refine'_1
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hnne0 : n ≠ 0
hgt : n < 0
h1n : n ≤ -1
⊢ a i ^ (-1) • X iᶜ ⊆ Y i
rw [zpow_neg, zpow_one]
no goals
case refine'_1
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hnne0 : n ≠ 0
hgt : n < 0
h1n : n ≤ -1
⊢ (a i)⁻¹ • X iᶜ ⊆ Y i
exact hY i
case refine'_2
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hnne0 : n ≠ 0
hgt : n < 0
h1n : n ≤ -1
⊢ ∀ (n : ℤ), n ≤ -1 → a i ^ n • X iᶜ ⊆ Y i → a i ^ (n - 1) • X iᶜ ⊆ Y i
case refine'_2
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hnne0 : n ≠ 0
hgt : n < 0
h1n : n ≤ -1
⊢ ∀ (n : ℤ), n ≤ -1 → (fun n => a i ^ n • X iᶜ ⊆ Y i) n → (fun n => a i ^ n • X iᶜ ⊆ Y i) (n - 1)
dsimp
case refine'_2
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n✝ : ℤ
hnne0 : n✝ ≠ 0
hgt : n✝ < 0
h1n : n✝ ≤ -1
n : ℤ
a✝ : n ≤ -1
hi : a i ^ n • X iᶜ ⊆ Y i
⊢ a i ^ (n - 1) • X iᶜ ⊆ Y i
case refine'_2
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hnne0 : n ≠ 0
hgt : n < 0
h1n : n ≤ -1
⊢ ∀ (n : ℤ), n ≤ -1 → a i ^ n • X iᶜ ⊆ Y i → a i ^ (n - 1) • X iᶜ ⊆ Y i
intro n _ hi
no goals
case refine'_2
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n✝ : ℤ
hnne0 : n✝ ≠ 0
hgt : n✝ < 0
h1n : n✝ ≤ -1
n : ℤ
a✝ : n ≤ -1
hi : a i ^ n • X iᶜ ⊆ Y i
⊢ a i ^ (n - 1) • X iᶜ ⊆ Y i
calc
  a i ^ (n - 1) • X iᶜ = (a i ^ n * (a i)⁻¹) • X iᶜ := by rw [zpow_sub, zpow_one]
  _ = a i ^ n • (a i)⁻¹ • X iᶜ := (MulAction.mul_smul _ _ _)
  _ ⊆ a i ^ n • Y i := (smul_set_mono <| hY i)
  _ ⊆ a i ^ n • X iᶜ := (smul_set_mono (hXYdisj i i).symm.subset_compl_right)
  _ ⊆ Y i := hi
no goals
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n✝ : ℤ
hnne0 : n✝ ≠ 0
hgt : n✝ < 0
h1n : n✝ ≤ -1
n : ℤ
a✝ : n ≤ -1
hi : a i ^ n • X iᶜ ⊆ Y i
⊢ a i ^ (n - 1) • X iᶜ = (a i ^ n * (a i)⁻¹) • X iᶜ
rw [zpow_sub, zpow_one]
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
inhabited_h : Inhabited ι
⊢ 3 ≤ (#ι) ∨ ∃ i, 3 ≤ (#H i)
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
⊢ 3 ≤ (#ι) ∨ ∃ i, 3 ≤ (#H i)
inhabit ι
case h
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
inhabited_h : Inhabited ι
⊢ ∃ i, 3 ≤ (#H i)
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
inhabited_h : Inhabited ι
⊢ 3 ≤ (#ι) ∨ ∃ i, 3 ≤ (#H i)
right
case h
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
inhabited_h : Inhabited ι
⊢ 3 ≤ (#H default)
case h
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
inhabited_h : Inhabited ι
⊢ ∃ i, 3 ≤ (#H i)
use Inhabited.default
case h
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
inhabited_h : Inhabited ι
⊢ 3 ≤ (#FreeGroup Unit)
case h
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
inhabited_h : Inhabited ι
⊢ 3 ≤ (#H default)
simp only
case h
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
inhabited_h : Inhabited ι
⊢ 3 ≤ ℵ₀
case h
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
inhabited_h : Inhabited ι
⊢ 3 ≤ (#FreeGroup Unit)
rw [FreeGroup.freeGroupUnitEquivInt.cardinal_eq, Cardinal.mk_denumerable]
case h.a
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
inhabited_h : Inhabited ι
⊢ 3 < ℵ₀
case h
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
inhabited_h : Inhabited ι
⊢ 3 ≤ ℵ₀
apply le_of_lt
no goals
case h.a
ι : Type u_2
M : ι → Type ?u.1007390
inst✝⁴ : (i : ι) → Monoid (M i)
N : Type ?u.1007401
inst✝³ : Monoid N
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type ?u.1007419
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), Set.Nonempty (X i)
hXdisj : Pairwise fun i j => Disjoint (X i) (X j)
hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • Y iᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • X iᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => ↑FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
inhabited_h : Inhabited ι
⊢ 3 < ℵ₀
exact nat_lt_aleph0 3