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
n : ℤ
hnne0 : n ≠ 0
hgt : n < 0
H₁ : n < HAdd.hAdd (α := ℤ) (-1) 1
⊢ n ≤ -1

Tactic:
apply Int.le_of_lt_add_one

Premises used: Int.le_of_lt_add_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 : ℤ
hnne0 : n ≠ 0
hgt : n < 0
⊢ n < HAdd.hAdd (α := ℤ) (-1) 1

Tactic:
simpa using hgt
-- 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
hgt : n < 0
⊢ n ≤ -1

Tactic:
have h1n : n ≤ -1 := by
        apply Int.le_of_lt_add_one
        simpa using hgt
-- 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
hgt : n < 0
h1n : n ≤ -1
⊢ a i ^ n • X' j ⊆ a i ^ n • (X i)ᶜ

Tactic:
smul_set_mono ((hXdisj hij.symm).union_left (hXYdisj i j).symm).subset_compl_right

Premises used: Disjoint.subset_compl_right, Ne.symm, Set.smul_set_mono, Disjoint.union_left, Disjoint.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 : ℤ
base : (a i)⁻¹ • (X i)ᶜ ⊆ Y i
⊢ HPow.hPow (β := ℤ) (a i) (-1) • (X i)ᶜ ⊆ Y i

Tactic:
rw [zpow_neg, zpow_one]

Premises used: zpow_one, zpow_neg
-- 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)⁻¹ • (X i)ᶜ ⊆ Y i

Tactic:
hY 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)⁻¹ • (X i)ᶜ ⊆ Y i

Tactic:
exact hY 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 : n ≤ -1
hi : a i ^ n • (X i)ᶜ ⊆ Y i
rw : (a i ^ n * (HPow.hPow (β := ℤ) (a i) 1)⁻¹) • (X i)ᶜ = (a i ^ n * (a i)⁻¹) • (X i)ᶜ
rw₁ rw₂ : (a i ^ n * (a i)⁻¹) • (X i)ᶜ = (a i ^ n * (a i)⁻¹) • (X i)ᶜ
⊢ a i ^ (n - 1) • (X i)ᶜ = (a i ^ n * (a i)⁻¹) • (X i)ᶜ

Tactic:
rw [zpow_sub, zpow_one]

Premises used: zpow_one, zpow_sub
-- 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 : n ≤ -1
hi : a i ^ n • (X i)ᶜ ⊆ Y i
⊢ (a i ^ n * (a i)⁻¹) • (X i)ᶜ = a i ^ n • (a i)⁻¹ • (X 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 : n ≤ -1
hi : a i ^ n • (X i)ᶜ ⊆ Y i
⊢ a i ^ n • (a i)⁻¹ • (X i)ᶜ ⊆ a i ^ n • Y i

Tactic:
smul_set_mono <| hY 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 : n ≤ -1
hi : a i ^ n • (X i)ᶜ ⊆ Y i
⊢ a i ^ n • Y i ⊆ a i ^ n • (X i)ᶜ

Tactic:
smul_set_mono (hXYdisj i i).symm.subset_compl_right

Premises used: Disjoint.subset_compl_right, Set.smul_set_mono, Disjoint.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_1 n : ℤ
hle : n ≤ -1
hi : a i ^ n • (X i)ᶜ ⊆ Y i
⊢ a i ^ n • (X i)ᶜ ⊆ Y 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 : n ≤ -1
hi : a i ^ n • (X i)ᶜ ⊆ Y i
a₁ : a i ^ (n - 1) • (X i)ᶜ = (a i ^ n * (a i)⁻¹) • (X i)ᶜ
⊢ a i ^ (n - 1) • (X i)ᶜ ⊆ Y i

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

Premises used: HMul.hMul, Disjoint.subset_compl_right, HSub.hSub, Set.smul_set_mono, Disjoint.symm, Inv.inv, HPow.hPow, 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 : n ≤ -1
base : HPow.hPow (β := ℤ) (a i) (-1) • (X i)ᶜ ⊆ Y i
pred : ∀ (n : ℤ) (hle : n ≤ -1) (hi : a i ^ n • (X i)ᶜ ⊆ Y i), a i ^ (n - 1) • (X i)ᶜ ⊆ Y i
⊢ a i ^ n • (X i)ᶜ ⊆ Y i

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

Premises used: HMul.hMul, Disjoint.subset_compl_right, HSub.hSub, zpow_one, Set.smul_set_mono, Disjoint.symm, Inv.inv, HPow.hPow, zpow_neg, 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
hgt : n < 0
h1n : n ≤ -1
⊢ Y i ⊆ X' i

Tactic:
Set.subset_union_right

Premises used: Set.subset_union_right
-- 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
hgt : n < 0
h1n : n ≤ -1
a₁ : a i ^ n • (X i)ᶜ ⊆ Y i
⊢ a i ^ n • (X j ∪ Y j) ⊆ X i ∪ Y i

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

Premises used: Disjoint.subset_compl_right, Set.subset_union_right, Ne.symm, Set.smul_set_mono, Disjoint.union_left, Disjoint.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
inhabit : ∀ (inhabited_h : Inhabited ι), 3 ≤ #ι ∨ ∃ (i : ι), 3 ≤ #(H i)
⊢ 3 ≤ #ι ∨ ∃ (i : ι), 3 ≤ #(H i)

Tactic:
inhabit ι
-- 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
inhabited_h : Inhabited ι
h : ∃ (i : ι), 3 ≤ #(H i)
⊢ 3 ≤ #ι ∨ ∃ (i : ι), 3 ≤ #(H i)

Tactic:
right
-- 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
inhabited_h : Inhabited ι
h : 3 ≤ #(H default)
⊢ ∃ (i : ι), 3 ≤ #(H i)

Tactic:
use Inhabited.default

Premises used: Inhabited.default
-- 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
inhabited_h : Inhabited ι
h : 3 ≤ #(FreeGroup Unit)
⊢ 3 ≤ #(H default)

Tactic:
simp only [H]
-- 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
inhabited_h : Inhabited ι
h : 3 ≤ ℵ₀
⊢ 3 ≤ #(FreeGroup Unit)

Tactic:
rw [FreeGroup.freeGroupUnitEquivInt.cardinal_eq, Cardinal.mk_denumerable]

Premises used: FreeGroup.freeGroupUnitEquivInt, Cardinal.mk_denumerable, Equiv.cardinal_eq
-- 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
inhabited_h : Inhabited ι
⊢ 3 ≤ ℵ₀

Tactic:
natCast_le_aleph0

Premises used: Cardinal.natCast_le_aleph0
-- 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
inhabited_h : Inhabited ι
⊢ 3 ≤ ℵ₀

Tactic:
exact natCast_le_aleph0

Premises used: Cardinal.natCast_le_aleph0
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Mul α
s : Set α
x a : α
hxS : x ∈ s
⊢ a * x ∈ a • s

Tactic:
mem_image_of_mem (fun b : α => a * b) hxS

Premises used: HMul.hMul, Set.Mem, Set.mem_image_of_mem
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Mul α
s : Set α
x a : α
hxS : x ∈ s
⊢ x * a ∈ op a • s

Tactic:
mem_image_of_mem (fun b : α => b * a) hxS

Premises used: HMul.hMul, Set.Mem, Set.mem_image_of_mem, MulOpposite.unop
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Mul α
s : Set α
⊢ Equivalence (LeftCosetEquivalence s)

Tactic:
@Equivalence.mk _ (LeftCosetEquivalence s) (fun _ => rfl) Eq.symm Eq.trans

Premises used: Equivalence.mk, Eq.symm, rfl, Eq.trans
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Mul α
s : Set α
⊢ Equivalence (RightCosetEquivalence s)

Tactic:
@Equivalence.mk _ (RightCosetEquivalence s) (fun _a => rfl) Eq.symm Eq.trans

Premises used: Equivalence.mk, Eq.symm, rfl, Eq.trans
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Semigroup α
s : Set α
a b : α
⊢ a • b • s = (a * b) • s

Tactic:
simp [← image_smul, (image_comp _ _ _).symm, Function.comp, mul_assoc]

Premises used: Set.image_smul, mul_assoc, Function.comp, Set.image_comp, Eq.symm
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Semigroup α
s : Set α
a b : α
⊢ op b • op a • s = op (a * b) • s

Tactic:
simp [← image_smul, (image_comp _ _ _).symm, Function.comp, mul_assoc]

Premises used: Set.image_smul, mul_assoc, Function.comp, Set.image_comp, Eq.symm
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Semigroup α
s : Set α
a b : α
⊢ op b • a • s = a • op b • s

Tactic:
simp [← image_smul, (image_comp _ _ _).symm, Function.comp, mul_assoc]

Premises used: Set.image_smul, mul_assoc, Function.comp, Set.image_comp, Eq.symm
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Monoid α
s : Set α
⊢ ∀ (x : α), x ∈ HSMul.hSMul (α := α) 1 s ↔ x ∈ s

Tactic:
simp
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Monoid α
s : Set α
⊢ ∀ (x : α), x ∈ HSMul.hSMul (α := αᵐᵒᵖ) (op 1) s ↔ x ∈ s

Tactic:
simp
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Monoid α
s : Submonoid α
a : α
this : a * 1 ∈ a • (↑s : Set α)
⊢ a ∈ a • (↑s : Set α)

Tactic:
simpa
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Monoid α
s : Submonoid α
a : α
this : 1 * a ∈ op a • (↑s : Set α)
⊢ a ∈ op a • (↑s : Set α)

Tactic:
simpa
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Monoid α
s : Submonoid α
a : α
ha : a • (↑s : Set α) = (↑s : Set α)
rw : a ∈ a • (↑s : Set α)
⊢ a ∈ s

Tactic:
rw [← SetLike.mem_coe, ← ha]

Premises used: SetLike.mem_coe
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Monoid α
s : Submonoid α
a : α
ha : a • (↑s : Set α) = (↑s : Set α)
⊢ a ∈ a • (↑s : Set α)

Tactic:
mem_own_leftCoset s a

Premises used: mem_own_leftCoset
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Monoid α
s : Submonoid α
a : α
ha : a • (↑s : Set α) = (↑s : Set α)
⊢ a ∈ a • (↑s : Set α)

Tactic:
exact mem_own_leftCoset s a

Premises used: mem_own_leftCoset
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Monoid α
s : Submonoid α
a : α
ha : op a • (↑s : Set α) = (↑s : Set α)
rw : a ∈ op a • (↑s : Set α)
⊢ a ∈ s

Tactic:
rw [← SetLike.mem_coe, ← ha]

Premises used: SetLike.mem_coe
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Monoid α
s : Submonoid α
a : α
ha : op a • (↑s : Set α) = (↑s : Set α)
⊢ a ∈ op a • (↑s : Set α)

Tactic:
mem_own_rightCoset s a

Premises used: mem_own_rightCoset
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Monoid α
s : Submonoid α
a : α
ha : op a • (↑s : Set α) = (↑s : Set α)
⊢ a ∈ op a • (↑s : Set α)

Tactic:
exact mem_own_rightCoset s a

Premises used: mem_own_rightCoset
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Set α
x a : α
h : x ∈ a • s
b : α
hb : b ∈ s
Eq : (fun (x : α) ↦ a • x) b = x
⊢ a⁻¹ * x ∈ s

Tactic:
simp [Eq.symm, hb]

Premises used: Eq.symm
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Set α
x a : α
h : a⁻¹ * x ∈ s
⊢ (fun (x : α) ↦ a • x) (a⁻¹ * x) = x

Tactic:
simp
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Set α
x a : α
h : x ∈ op a • s
b : α
hb : b ∈ s
Eq : (fun (x : α) ↦ op a • x) b = x
⊢ x * a⁻¹ ∈ s

Tactic:
simp [Eq.symm, hb]

Premises used: Eq.symm
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Set α
x a : α
h : x * a⁻¹ ∈ s
⊢ (fun (x : α) ↦ op a • x) (x * a⁻¹) = x

Tactic:
simp