Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case hpp
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
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 := ⋯
f : (i : ι) → H i →* G := ⋯
X' : ι → Set α := ⋯
⊢ Pairwise fun i j ↦ ∀ (h : H i), h ≠ 1 → (f i) h • X' j ⊆ X' i

pp: ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
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 := ⋯
f : (i : ι) → H i →* G := ⋯
X' : ι → Set α := ⋯
⊢ 3 ≤ #ι ∨ ∃ i, 3 ≤ #(H i)

Tactic:
· change Pairwise fun i j => ∀ h : H i, h ≠ 1 → f i h • X' j ⊆ X' i
    rintro i j hij
    -- use free_group unit ≃ ℤ
    refine FreeGroup.freeGroupUnitEquivInt.forall_congr_left.mpr ?_
    intro n hne1
    change FreeGroup.lift (fun _ => a i) (FreeGroup.of () ^ n) • X' j ⊆ X' i
    simp only [map_zpow, FreeGroup.lift_apply_of]
    change a i ^ n • X' j ⊆ X' i
    have hnne0 : n ≠ 0 := by
      rintro rfl
      apply hne1
      simp [H, FreeGroup.freeGroupUnitEquivInt]
    clear hne1
    simp only [X']
    -- Positive and negative powers separately
    rcases (lt_or_gt_of_ne hnne0).symm with hlt | hgt
    · have h1n : 1 ≤ n := hlt
      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
          induction n, h1n using Int.leInduction with
          | base => rw [zpow_one]; exact hX i
          | succ 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)ᶜ := 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
    · have h1n : n ≤ -1 := by
        apply Int.le_of_lt_add_one
        simpa using hgt
      calc
        a i ^ n • X' j ⊆ a i ^ n • (X i)ᶜ :=
          smul_set_mono ((hXdisj hij.symm).union_left (hXYdisj i j).symm).subset_compl_right
        _ ⊆ Y i := by
          clear hnne0 hgt
          induction n, h1n using Int.leInductionDown with
          | base => rw [zpow_neg, zpow_one]; exact hY i
          | pred n hle hi =>
            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)ᶜ := 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
        _ ⊆ X' i := Set.subset_union_right

Goal state after:
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
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 := ⋯
f : (i : ι) → H i →* G := ⋯
X' : ι → Set α := ⋯
⊢ 3 ≤ #ι ∨ ∃ i, 3 ≤ #(H i)