awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
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
⊢ a i ^ n • (X j ∪ Y j) ⊆ X i ∪ Y i
have hpp₁ : ∀ (hgt : n < 0), a i ^ n • (X j ∪ Y j) ⊆ X i ∪ Y i
Tactic: rcases (lt_or_gt_of_ne hnne0).symm with hlt | hgt
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (hypothesis)
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
⊢ a i ^ n • (X j ∪ Y j) ⊆ X i ∪ Y i
have h1n : 1 ≤ n
Tactic: have h1n : 1 ≤ n := hlt
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
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 : ℤ
⊢ HPow.hPow (β := ℤ) (a i) 1 • (Y i)ᶜ ⊆ X i
have base : a i • (Y i)ᶜ ⊆ X i
Tactic: rw [zpow_one]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
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 + 1) • (Y i)ᶜ = (a i ^ n * a i) • (Y i)ᶜ
have rw : (a i ^ n * HPow.hPow (β := ℤ) (a i) 1) • (Y i)ᶜ = (a i ^ n * a i) • (Y i)ᶜ
Tactic: rw [zpow_add, zpow_one]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
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)ᶜ
⊢ a i ^ (n + 1) • (Y i)ᶜ = (a i ^ n * a i) • (Y i)ᶜ
have rw₁ : (a i ^ n * a i) • (Y i)ᶜ = (a i ^ n * a i) • (Y i)ᶜ
Tactic: rw [zpow_add, zpow_one]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
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 + 1) • (Y i)ᶜ ⊆ X i
have a₁ : a i ^ (n + 1) • (Y i)ᶜ = (a i ^ n * a i) • (Y 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
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
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
⊢ a i ^ n • (Y i)ᶜ ⊆ X i
have base : HPow.hPow (β := ℤ) (a i) 1 • (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
Cleared hypotheses: h1n
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
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
⊢ a i ^ n • (Y i)ᶜ ⊆ X i
have succ : ∀ (n : ℤ) (_hle : 1 ≤ n) (hi : a i ^ n • (Y i)ᶜ ⊆ X i), a i ^ (n + 1) • (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
Cleared hypotheses: h1n
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
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 ∪ Y j) ⊆ X i ∪ Y i
have a₁ : a i ^ n • (Y i)ᶜ ⊆ X 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
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
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
have H₁ : n < HAdd.hAdd (α := ℤ) (-1) 1
Tactic: apply Int.le_of_lt_add_one
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (hypothesis)
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
⊢ a i ^ n • (X j ∪ Y j) ⊆ X i ∪ Y i
have h1n : n ≤ -1
Tactic: have h1n : n ≤ -1 := by
        apply Int.le_of_lt_add_one
        simpa using hgt
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
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 : ℤ
⊢ HPow.hPow (β := ℤ) (a i) (-1) • (X i)ᶜ ⊆ Y i
have base : (a i)⁻¹ • (X i)ᶜ ⊆ Y i
Tactic: rw [zpow_neg, zpow_one]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
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 - 1) • (X i)ᶜ = (a i ^ n * (a i)⁻¹) • (X i)ᶜ
have rw : (a i ^ n * (HPow.hPow (β := ℤ) (a i) 1)⁻¹) • (X i)ᶜ = (a i ^ n * (a i)⁻¹) • (X i)ᶜ
Tactic: rw [zpow_sub, zpow_one]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
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)ᶜ
⊢ a i ^ (n - 1) • (X i)ᶜ = (a i ^ n * (a i)⁻¹) • (X i)ᶜ
have rw₁ : (a i ^ n * (a i)⁻¹) • (X i)ᶜ = (a i ^ n * (a i)⁻¹) • (X i)ᶜ
Tactic: rw [zpow_sub, zpow_one]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
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 - 1) • (X i)ᶜ ⊆ Y i
have a₁ : a i ^ (n - 1) • (X i)ᶜ = (a i ^ n * (a i)⁻¹) • (X 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
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
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
⊢ a i ^ n • (X i)ᶜ ⊆ Y i
have base : HPow.hPow (β := ℤ) (a i) (-1) • (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
Cleared hypotheses: h1n
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
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
⊢ a i ^ n • (X i)ᶜ ⊆ Y i
have pred : ∀ (n : ℤ) (hle : n ≤ -1) (hi : a i ^ n • (X i)ᶜ ⊆ Y i), a i ^ (n - 1) • (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
Cleared hypotheses: h1n
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
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 ∪ Y j) ⊆ X i ∪ Y i
have a₁ : a i ^ n • (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
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
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
⊢ 3 ≤ #ι ∨ ∃ (i : ι), 3 ≤ #(H i)
have inhabit : ∀ (inhabited_h : Inhabited ι), 3 ≤ #ι ∨ ∃ (i : ι), 3 ≤ #(H i)
Tactic: inhabit ι
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
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 ≤ #ι ∨ ∃ (i : ι), 3 ≤ #(H i)
have h : ∃ (i : ι), 3 ≤ #(H i)
Tactic: right
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
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 ι
⊢ ∃ (i : ι), 3 ≤ #(H i)
have h : 3 ≤ #(H default)
Tactic: use Inhabited.default
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
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 ≤ #(FreeGroup Unit)
have h : 3 ≤ ℵ₀
Tactic: rw [FreeGroup.freeGroupUnitEquivInt.cardinal_eq, Cardinal.mk_denumerable]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Monoid α
s : Submonoid α
a : α
ha : a • (↑s : Set α) = (↑s : Set α)
⊢ a ∈ s
have rw : a ∈ a • (↑s : Set α)
Tactic: rw [← SetLike.mem_coe, ← ha]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Monoid α
s : Submonoid α
a : α
ha : op a • (↑s : Set α) = (↑s : Set α)
⊢ a ∈ s
have rw : a ∈ op a • (↑s : Set α)
Tactic: rw [← SetLike.mem_coe, ← ha]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
h : ∀ (g : α), g • (↑s : Set α) = op g • (↑s : Set α)
a : α
ha : a ∈ s
g : α
⊢ g * a * g⁻¹ ∈ (↑s : Set α)
have rw : g * a ∈ g • (↑s : Set α)
Tactic: rw [← mem_rightCoset_iff, ← h]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x y : α
⊢ x • (↑s : Set α) = y • (↑s : Set α) ↔ x⁻¹ * y ∈ s
have rw : (∀ (x_1 : α), x_1 ∈ x • (↑s : Set α) ↔ x_1 ∈ y • (↑s : Set α)) ↔ x⁻¹ * y ∈ s
Tactic: rw [Set.ext_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x y : α
⊢ (∀ (x_1 : α), x_1 ∈ x • (↑s : Set α) ↔ x_1 ∈ y • (↑s : Set α)) ↔ x⁻¹ * y ∈ s
have simp_rw : (∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s) ↔ x⁻¹ * y ∈ s
Tactic: simp_rw [mem_leftCoset_iff, SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x y : α
⊢ (∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s) ↔ x⁻¹ * y ∈ s
have mp : (∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s) → x⁻¹ * y ∈ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x y : α
mp : (∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s) → x⁻¹ * y ∈ s
⊢ (∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s) ↔ x⁻¹ * y ∈ s
have mpr : x⁻¹ * y ∈ s → ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x y : α
h : ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s
⊢ x⁻¹ * y ∈ s
have mp : y⁻¹ * y ∈ s
Tactic: apply (h y).mpr
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x y : α
h : ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s
⊢ y⁻¹ * y ∈ s
have mp : 1 ∈ s
Tactic: rw [inv_mul_cancel]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x y : α
h : x⁻¹ * y ∈ s
z : α
⊢ x⁻¹ * z ∈ s ↔ y⁻¹ * z ∈ s
have mpr : x⁻¹ * y * y⁻¹ * z ∈ s ↔ y⁻¹ * z ∈ s
Tactic: rw [← mul_inv_cancel_right x⁻¹ y]