awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
inst : Nontrivial ι
G : Type u_1
inst_1 : Group G
a : ι → G
α : Type u_4
inst_2 : 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 := fun (_i : ι) ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun (i : ι) ↦ (FreeGroup.lift : (a : Unit → G) → FreeGroup Unit →* G) fun (x : Unit) ↦ a i
X' : ι → Set α := fun (i : ι) ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
⊢ Disjoint (Y i) (Y j)

Tactic:
hYdisj hij
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
inst : Nontrivial ι
G : Type u_1
inst_1 : Group G
a : ι → G
α : Type u_4
inst_2 : 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 := fun (_i : ι) ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun (i : ι) ↦ (FreeGroup.lift : (a : Unit → G) → FreeGroup Unit →* G) fun (x : Unit) ↦ a i
X' : ι → Set α := fun (i : ι) ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
⊢ Disjoint (Y i) (Y j)

Tactic:
exact hYdisj hij
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
inst : Nontrivial ι
G : Type u_1
inst_1 : Group G
a : ι → G
α : Type u_4
inst_2 : 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 := fun (_i : ι) ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun (i : ι) ↦ (FreeGroup.lift : (a : Unit → G) → FreeGroup Unit →* G) fun (x : Unit) ↦ a i
X' : ι → Set α := fun (i : ι) ↦ X i ∪ Y i
hpp : Pairwise fun (i j : ι) ↦ ∀ (h : H i), h ≠ 1 → HSMul.hSMul (α := G) ((f i : (a : H i) → G) h : G) (X' j) ⊆ X' i
⊢ Pairwise fun (i j : ι) ↦ ∀ (h : H i), h ≠ 1 → HSMul.hSMul (α := G) ((f i : (a : H i) → G) h : G) (X' j) ⊆ X' i

Tactic:
change Pairwise fun i j => ∀ h : H i, h ≠ 1 → f i h • X' j ⊆ X' i

Premises used: Pairwise
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
inst : Nontrivial ι
G : Type u_1
inst_1 : Group G
a : ι → G
α : Type u_4
inst_2 : 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 := fun (_i : ι) ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun (i : ι) ↦ (FreeGroup.lift : (a : Unit → G) → FreeGroup Unit →* G) fun (x : Unit) ↦ a i
X' : ι → Set α := fun (i : ι) ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
⊢ ∀ (h : H i), h ≠ 1 → HSMul.hSMul (α := G) ((f i : (a : H i) → G) h : G) (X' j) ⊆ X' i

Tactic:
FreeGroup.freeGroupUnitEquivInt.forall_congr_left.mpr ?_

Premises used: Iff.mpr, Equiv.forall_congr_left, FreeGroup.freeGroupUnitEquivInt
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
inst : Nontrivial ι
G : Type u_1
inst_1 : Group G
a : ι → G
α : Type u_4
inst_2 : 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 := fun (_i : ι) ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun (i : ι) ↦ (FreeGroup.lift : (a : Unit → G) → FreeGroup Unit →* G) fun (x : Unit) ↦ a i
X' : ι → Set α := fun (i : ι) ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
hpp :
  ∀ (b : ℤ),
    Ne (α := H i) ((FreeGroup.freeGroupUnitEquivInt.symm : (a : ℤ) → FreeGroup Unit) b : FreeGroup Unit) (1 : H i) →
      HSMul.hSMul (α := G)
          ((f i : (a : H i) → G)
              ((FreeGroup.freeGroupUnitEquivInt.symm : (a : ℤ) → FreeGroup Unit) b : FreeGroup Unit) :
            G)
          (X' j) ⊆
        X' i
⊢ ∀ (h : H i), h ≠ 1 → HSMul.hSMul (α := G) ((f i : (a : H i) → G) h : G) (X' j) ⊆ X' i

Tactic:
refine FreeGroup.freeGroupUnitEquivInt.forall_congr_left.mpr ?_

Premises used: Iff.mpr, Equiv.forall_congr_left, FreeGroup.freeGroupUnitEquivInt
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
inst : Nontrivial ι
G : Type u_1
inst_1 : Group G
a : ι → G
α : Type u_4
inst_2 : 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 := fun (_i : ι) ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun (i : ι) ↦ (FreeGroup.lift : (a : Unit → G) → FreeGroup Unit →* G) fun (x : Unit) ↦ a i
X' : ι → Set α := fun (i : ι) ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hne1 : Ne (α := H i) ((FreeGroup.freeGroupUnitEquivInt.symm : (a : ℤ) → FreeGroup Unit) n : FreeGroup Unit) (1 : H i)
hpp :
  HSMul.hSMul.{u_1, u_4, u_4} (α := G)
      (((FreeGroup.lift : (a : Unit → G) → FreeGroup Unit →* G) fun (x : Unit) ↦ a i : (a : FreeGroup Unit) → G)
          (FreeGroup.of () ^ n) :
        G)
      (X' j) ⊆
    X' i
⊢ HSMul.hSMul (α := G)
      ((f i : (a : H i) → G) ((FreeGroup.freeGroupUnitEquivInt.symm : (a : ℤ) → FreeGroup Unit) n : FreeGroup Unit) : G)
      (X' j) ⊆
    X' i

Tactic:
change FreeGroup.lift (fun _ => a i) (FreeGroup.of () ^ n) • X' j ⊆ X' i

Premises used: FreeGroup.of, Unit.unit, FreeGroup.lift, HPow.hPow, DFunLike.coe
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
inst : Nontrivial ι
G : Type u_1
inst_1 : Group G
a : ι → G
α : Type u_4
inst_2 : 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 := fun (_i : ι) ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun (i : ι) ↦ (FreeGroup.lift : (a : Unit → G) → FreeGroup Unit →* G) fun (x : Unit) ↦ a i
X' : ι → Set α := fun (i : ι) ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hne1 : Ne (α := H i) ((FreeGroup.freeGroupUnitEquivInt.symm : (a : ℤ) → FreeGroup Unit) n : FreeGroup Unit) (1 : H i)
hpp : a i ^ n • X' j ⊆ X' i
⊢ HSMul.hSMul.{u_1, u_4, u_4} (α := G)
      (((FreeGroup.lift : (a : Unit → G) → FreeGroup Unit →* G) fun (x : Unit) ↦ a i : (a : FreeGroup Unit) → G)
          (FreeGroup.of () ^ n) :
        G)
      (X' j) ⊆
    X' i

Tactic:
simp only [map_zpow, FreeGroup.lift_apply_of]

Premises used: FreeGroup.lift_apply_of, map_zpow
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
inst : Nontrivial ι
G : Type u_1
inst_1 : Group G
a : ι → G
α : Type u_4
inst_2 : 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 := fun (_i : ι) ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun (i : ι) ↦ (FreeGroup.lift : (a : Unit → G) → FreeGroup Unit →* G) fun (x : Unit) ↦ a i
X' : ι → Set α := fun (i : ι) ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hne1 : Ne (α := H i) ((FreeGroup.freeGroupUnitEquivInt.symm : (a : ℤ) → FreeGroup Unit) n : FreeGroup Unit) (1 : H i)
hpp : a i ^ n • X' j ⊆ X' i
⊢ a i ^ n • X' j ⊆ X' i

Tactic:
change a i ^ n • X' j ⊆ X' i
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
inst : Nontrivial ι
G : Type u_1
inst_1 : Group G
a : ι → G
α : Type u_4
inst_2 : 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 := fun (_i : ι) ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun (i : ι) ↦ (FreeGroup.lift : (a : Unit → G) → FreeGroup Unit →* G) fun (x : Unit) ↦ a i
X' : ι → Set α := fun (i : ι) ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
hne1 : Ne (α := H i) ((FreeGroup.freeGroupUnitEquivInt.symm : (a : ℤ) → FreeGroup Unit) 0) 1
apply : Eq (α := H i) ((FreeGroup.freeGroupUnitEquivInt.symm : (a : ℤ) → FreeGroup Unit) 0) 1
⊢ False

Tactic:
apply hne1
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
inst : Nontrivial ι
G : Type u_1
inst_1 : Group G
a : ι → G
α : Type u_4
inst_2 : 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 := fun (_i : ι) ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun (i : ι) ↦ (FreeGroup.lift : (a : Unit → G) → FreeGroup Unit →* G) fun (x : Unit) ↦ a i
X' : ι → Set α := fun (i : ι) ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
hne1 : Ne (α := H i) ((FreeGroup.freeGroupUnitEquivInt.symm : (a : ℤ) → FreeGroup Unit) 0) 1
⊢ Eq (α := H i) ((FreeGroup.freeGroupUnitEquivInt.symm : (a : ℤ) → FreeGroup Unit) 0) 1

Tactic:
simp [H, FreeGroup.freeGroupUnitEquivInt]

Premises used: FreeGroup.freeGroupUnitEquivInt
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
inst : Nontrivial ι
G : Type u_1
inst_1 : Group G
a : ι → G
α : Type u_4
inst_2 : 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 := fun (_i : ι) ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun (i : ι) ↦ (FreeGroup.lift : (a : Unit → G) → FreeGroup Unit →* G) fun (x : Unit) ↦ a i
X' : ι → Set α := fun (i : ι) ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hne1 : Ne (α := H i) ((FreeGroup.freeGroupUnitEquivInt.symm : (a : ℤ) → FreeGroup Unit) n : FreeGroup Unit) (1 : H i)
⊢ n ≠ 0

Tactic:
have hnne0 : n ≠ 0 := by
      rintro rfl
      apply hne1
      simp [H, FreeGroup.freeGroupUnitEquivInt]
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
inst : Nontrivial ι
G : Type u_1
inst_1 : Group G
a : ι → G
α : Type u_4
inst_2 : 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 := fun (_i : ι) ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun (i : ι) ↦ (FreeGroup.lift : (a : Unit → G) → FreeGroup Unit →* G) fun (x : Unit) ↦ a i
X' : ι → Set α := fun (i : ι) ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hnne0 : n ≠ 0
hpp : a i ^ n • (X j ∪ Y j) ⊆ X i ∪ Y i
⊢ a i ^ n • X' j ⊆ X' i

Tactic:
simp only [X']
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
inst : Nontrivial ι
G : Type u_1
inst_1 : Group G
a : ι → G
α : Type u_4
inst_2 : 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 := fun (_i : ι) ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun (i : ι) ↦ (FreeGroup.lift : (a : Unit → G) → FreeGroup Unit →* G) fun (x : Unit) ↦ a i
X' : ι → Set α := fun (i : ι) ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hnne0 : n ≠ 0
hpp : ∀ (hlt : 0 < n), a i ^ n • (X j ∪ Y j) ⊆ X i ∪ Y i
hpp₁ : ∀ (hgt : n < 0), a i ^ n • (X j ∪ Y j) ⊆ X i ∪ Y i
⊢ a i ^ n • (X j ∪ Y j) ⊆ X i ∪ Y i

Tactic:
rcases (lt_or_gt_of_ne hnne0).symm with hlt | hgt

Premises used: lt_or_gt_of_ne, Or.symm
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
inst : Nontrivial ι
G : Type u_1
inst_1 : Group G
a : ι → G
α : Type u_4
inst_2 : 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 := fun (_i : ι) ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun (i : ι) ↦ (FreeGroup.lift : (a : Unit → G) → FreeGroup Unit →* G) fun (x : Unit) ↦ a i
X' : ι → Set α := fun (i : ι) ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hnne0 : n ≠ 0
hlt : 0 < n
⊢ 1 ≤ n

Tactic:
have h1n : 1 ≤ n := hlt
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
inst : Nontrivial ι
G : Type u_1
inst_1 : Group G
a : ι → G
α : Type u_4
inst_2 : 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 := fun (_i : ι) ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun (i : ι) ↦ (FreeGroup.lift : (a : Unit → G) → FreeGroup Unit →* G) fun (x : Unit) ↦ a i
X' : ι → Set α := fun (i : ι) ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hnne0 : n ≠ 0
hlt : 0 < n
h1n : 1 ≤ n
⊢ a i ^ n • X' j ⊆ a i ^ n • (Y i)ᶜ

Tactic:
smul_set_mono ((hXYdisj j i).union_left <| hYdisj hij.symm).subset_compl_right

Premises used: Disjoint.subset_compl_right, Ne.symm, Set.smul_set_mono, Disjoint.union_left
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
inst : Nontrivial ι
G : Type u_1
inst_1 : Group G
a : ι → G
α : Type u_4
inst_2 : 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 := fun (_i : ι) ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun (i : ι) ↦ (FreeGroup.lift : (a : Unit → G) → FreeGroup Unit →* G) fun (x : Unit) ↦ a i
X' : ι → Set α := fun (i : ι) ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
base : a i • (Y i)ᶜ ⊆ X i
⊢ HPow.hPow (β := ℤ) (a i) 1 • (Y i)ᶜ ⊆ X i

Tactic:
rw [zpow_one]

Premises used: zpow_one
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
inst : Nontrivial ι
G : Type u_1
inst_1 : Group G
a : ι → G
α : Type u_4
inst_2 : 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 := fun (_i : ι) ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun (i : ι) ↦ (FreeGroup.lift : (a : Unit → G) → FreeGroup Unit →* G) fun (x : Unit) ↦ a i
X' : ι → Set α := fun (i : ι) ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
⊢ a i • (Y i)ᶜ ⊆ X i

Tactic:
hX i
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
inst : Nontrivial ι
G : Type u_1
inst_1 : Group G
a : ι → G
α : Type u_4
inst_2 : 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 := fun (_i : ι) ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun (i : ι) ↦ (FreeGroup.lift : (a : Unit → G) → FreeGroup Unit →* G) fun (x : Unit) ↦ a i
X' : ι → Set α := fun (i : ι) ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
⊢ a i • (Y i)ᶜ ⊆ X i

Tactic:
exact hX i
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
inst : Nontrivial ι
G : Type u_1
inst_1 : Group G
a : ι → G
α : Type u_4
inst_2 : 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 := fun (_i : ι) ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun (i : ι) ↦ (FreeGroup.lift : (a : Unit → G) → FreeGroup Unit →* G) fun (x : Unit) ↦ a i
X' : ι → Set α := fun (i : ι) ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
n_1 n : ℤ
_hle : 1 ≤ n
hi : a i ^ n • (Y i)ᶜ ⊆ X i
rw : (a i ^ n * HPow.hPow (β := ℤ) (a i) 1) • (Y i)ᶜ = (a i ^ n * a i) • (Y i)ᶜ
rw₁ rw₂ : (a i ^ n * a i) • (Y i)ᶜ = (a i ^ n * a i) • (Y i)ᶜ
⊢ a i ^ (n + 1) • (Y i)ᶜ = (a i ^ n * a i) • (Y i)ᶜ

Tactic:
rw [zpow_add, zpow_one]

Premises used: zpow_add, zpow_one
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
inst : Nontrivial ι
G : Type u_1
inst_1 : Group G
a : ι → G
α : Type u_4
inst_2 : 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 := fun (_i : ι) ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun (i : ι) ↦ (FreeGroup.lift : (a : Unit → G) → FreeGroup Unit →* G) fun (x : Unit) ↦ a i
X' : ι → Set α := fun (i : ι) ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
n_1 n : ℤ
_hle : 1 ≤ n
hi : a i ^ n • (Y i)ᶜ ⊆ X i
⊢ (a i ^ n * a i) • (Y i)ᶜ = a i ^ n • a i • (Y i)ᶜ

Tactic:
mul_smul _ _ _

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
inst : Nontrivial ι
G : Type u_1
inst_1 : Group G
a : ι → G
α : Type u_4
inst_2 : 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 := fun (_i : ι) ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun (i : ι) ↦ (FreeGroup.lift : (a : Unit → G) → FreeGroup Unit →* G) fun (x : Unit) ↦ a i
X' : ι → Set α := fun (i : ι) ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
n_1 n : ℤ
_hle : 1 ≤ n
hi : a i ^ n • (Y i)ᶜ ⊆ X i
⊢ a i ^ n • a i • (Y i)ᶜ ⊆ a i ^ n • X i

Tactic:
smul_set_mono <| hX i

Premises used: Set.smul_set_mono
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
inst : Nontrivial ι
G : Type u_1
inst_1 : Group G
a : ι → G
α : Type u_4
inst_2 : 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 := fun (_i : ι) ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun (i : ι) ↦ (FreeGroup.lift : (a : Unit → G) → FreeGroup Unit →* G) fun (x : Unit) ↦ a i
X' : ι → Set α := fun (i : ι) ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
n_1 n : ℤ
_hle : 1 ≤ n
hi : a i ^ n • (Y i)ᶜ ⊆ X i
⊢ a i ^ n • X i ⊆ a i ^ n • (Y i)ᶜ

Tactic:
smul_set_mono (hXYdisj i i).subset_compl_right

Premises used: Disjoint.subset_compl_right, Set.smul_set_mono
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
inst : Nontrivial ι
G : Type u_1
inst_1 : Group G
a : ι → G
α : Type u_4
inst_2 : 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 := fun (_i : ι) ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun (i : ι) ↦ (FreeGroup.lift : (a : Unit → G) → FreeGroup Unit →* G) fun (x : Unit) ↦ a i
X' : ι → Set α := fun (i : ι) ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
n_1 n : ℤ
_hle : 1 ≤ n
hi : a i ^ n • (Y i)ᶜ ⊆ X i
⊢ a i ^ n • (Y i)ᶜ ⊆ X i

Tactic:
hi
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
inst : Nontrivial ι
G : Type u_1
inst_1 : Group G
a : ι → G
α : Type u_4
inst_2 : 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 := fun (_i : ι) ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun (i : ι) ↦ (FreeGroup.lift : (a : Unit → G) → FreeGroup Unit →* G) fun (x : Unit) ↦ a i
X' : ι → Set α := fun (i : ι) ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
n_1 n : ℤ
_hle : 1 ≤ n
hi : a i ^ n • (Y i)ᶜ ⊆ X i
a₁ : a i ^ (n + 1) • (Y i)ᶜ = (a i ^ n * a i) • (Y i)ᶜ
⊢ a i ^ (n + 1) • (Y i)ᶜ ⊆ X i

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

Premises used: HMul.hMul, Disjoint.subset_compl_right, Set.smul_set_mono, HPow.hPow, HAdd.hAdd, OfNat.ofNat, SemigroupAction.mul_smul
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
inst : Nontrivial ι
G : Type u_1
inst_1 : Group G
a : ι → G
α : Type u_4
inst_2 : 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 := fun (_i : ι) ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun (i : ι) ↦ (FreeGroup.lift : (a : Unit → G) → FreeGroup Unit →* G) fun (x : Unit) ↦ a i
X' : ι → Set α := fun (i : ι) ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
h1n : 1 ≤ n
base : HPow.hPow (β := ℤ) (a i) 1 • (Y i)ᶜ ⊆ X i
succ : ∀ (n : ℤ) (_hle : 1 ≤ n) (hi : a i ^ n • (Y i)ᶜ ⊆ X i), a i ^ (n + 1) • (Y i)ᶜ ⊆ X i
⊢ a i ^ n • (Y i)ᶜ ⊆ X i

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

Premises used: HMul.hMul, Disjoint.subset_compl_right, zpow_one, Set.smul_set_mono, HPow.hPow, HAdd.hAdd, OfNat.ofNat, SemigroupAction.mul_smul
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
inst : Nontrivial ι
G : Type u_1
inst_1 : Group G
a : ι → G
α : Type u_4
inst_2 : 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 := fun (_i : ι) ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun (i : ι) ↦ (FreeGroup.lift : (a : Unit → G) → FreeGroup Unit →* G) fun (x : Unit) ↦ a i
X' : ι → Set α := fun (i : ι) ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hnne0 : n ≠ 0
hlt : 0 < n
h1n : 1 ≤ n
⊢ X i ⊆ X' i

Tactic:
Set.subset_union_left

Premises used: Set.subset_union_left
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
inst : Nontrivial ι
G : Type u_1
inst_1 : Group G
a : ι → G
α : Type u_4
inst_2 : 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 := fun (_i : ι) ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun (i : ι) ↦ (FreeGroup.lift : (a : Unit → G) → FreeGroup Unit →* G) fun (x : Unit) ↦ a i
X' : ι → Set α := fun (i : ι) ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hnne0 : n ≠ 0
hlt : 0 < n
h1n : 1 ≤ n
a₁ : a i ^ n • (Y i)ᶜ ⊆ X i
⊢ a i ^ n • (X j ∪ Y j) ⊆ X i ∪ Y i

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

Premises used: Disjoint.subset_compl_right, Ne.symm, Set.smul_set_mono, Disjoint.union_left, Set.subset_union_left