awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι_1 : Type u_1
M : ι_1 → Type u_2
inst : (i : ι_1) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
ι : Type u_1
⊢ Eq.{u_1 + 1} (α := (CoprodI fun (x : ι) ↦ FreeGroup Unit) →* CoprodI fun (x : ι) ↦ FreeGroup Unit)
    (MonoidHom.comp (N := FreeGroup ι)
      ((FreeGroup.lift :
          (a : ι → CoprodI fun (x : ι) ↦ FreeGroup Unit) → FreeGroup ι →* CoprodI fun (x : ι) ↦ FreeGroup Unit)
        fun (i : ι) ↦
        ((of (M := fun (x : ι) ↦ FreeGroup Unit) (i := i) : FreeGroup Unit →* CoprodI fun (x : ι) ↦ FreeGroup Unit) :
            (a : FreeGroup Unit) → CoprodI fun (x : ι) ↦ FreeGroup Unit)
          (FreeGroup.of ()))
      ((lift (M := fun (x : ι) ↦ FreeGroup Unit) :
          (a : (i : ι) → FreeGroup Unit →* FreeGroup ι) → (CoprodI fun (x : ι) ↦ FreeGroup Unit) →* FreeGroup ι)
        fun (i : ι) ↦
        (FreeGroup.lift : (a : Unit → FreeGroup ι) → FreeGroup Unit →* FreeGroup ι) fun (x : Unit) ↦ FreeGroup.of i))
    (MonoidHom.id (CoprodI fun (x : ι) ↦ FreeGroup Unit))
have refine_4 : ∀ (i : ι) (a : Unit),
  Eq.{u_1 + 1} (α := CoprodI fun (x : ι) ↦ FreeGroup Unit)
    (((MonoidHom.comp (N := CoprodI fun (x : ι) ↦ FreeGroup Unit)
              (MonoidHom.comp (N := FreeGroup ι)
                ((FreeGroup.lift :
                    (a : ι → CoprodI fun (x : ι) ↦ FreeGroup Unit) →
                      FreeGroup ι →* CoprodI fun (x : ι) ↦ FreeGroup Unit)
                  fun (i : ι) ↦
                  ((of (M := fun (x : ι) ↦ FreeGroup Unit) (i := i) :
                        FreeGroup Unit →* CoprodI fun (x : ι) ↦ FreeGroup Unit) :
                      (a : FreeGroup Unit) → CoprodI fun (x : ι) ↦ FreeGroup Unit)
                    (FreeGroup.of ()))
                ((lift (M := fun (x : ι) ↦ FreeGroup Unit) :
                    (a : (i : ι) → FreeGroup Unit →* FreeGroup ι) →
                      (CoprodI fun (x : ι) ↦ FreeGroup Unit) →* FreeGroup ι)
                  fun (i : ι) ↦
                  (FreeGroup.lift : (a : Unit → FreeGroup ι) → FreeGroup Unit →* FreeGroup ι) fun (x : Unit) ↦
                    FreeGroup.of i))
              (of (M := fun (x : ι) ↦ FreeGroup Unit) (i := i)) :
            FreeGroup Unit →* CoprodI fun (x : ι) ↦ FreeGroup Unit) :
          (a : FreeGroup Unit) → CoprodI fun (x : ι) ↦ FreeGroup Unit)
        (FreeGroup.of a) :
      CoprodI fun (x : ι) ↦ FreeGroup Unit)
    (((MonoidHom.comp (MonoidHom.id (CoprodI fun (x : ι) ↦ FreeGroup Unit))
              (of (M := fun (x : ι) ↦ FreeGroup Unit) (i := i)) :
            FreeGroup Unit →* CoprodI fun (x : ι) ↦ FreeGroup Unit) :
          (a : FreeGroup Unit) → CoprodI fun (x : ι) ↦ FreeGroup Unit)
        (FreeGroup.of a) :
      CoprodI fun (x : ι) ↦ FreeGroup Unit)
Tactic: ext i a
-- 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
⊢ Eq (α := FreeGroup ι →* G) ((FreeGroup.lift : (a : ι → G) → FreeGroup ι →* G) a : FreeGroup ι →* G)
    (MonoidHom.comp
        ((lift (M := fun (i : ι) ↦ FreeGroup Unit) :
            (a : (i : ι) → FreeGroup Unit →* G) → (CoprodI fun (i : ι) ↦ FreeGroup Unit) →* G)
          fun (i : ι) ↦ (FreeGroup.lift : (a : Unit → G) → FreeGroup Unit →* G) fun (x : Unit) ↦ a i)
        (MulEquiv.toMonoidHom freeGroupEquivCoprodI) :
      FreeGroup ι →* G)
have h : ∀ (i : ι),
  Eq (α := G)
    ((((FreeGroup.lift : (a : ι → G) → FreeGroup ι →* G) a : FreeGroup ι →* G) : (a : FreeGroup ι) → G)
        (FreeGroup.of i) :
      G)
    ((MonoidHom.comp
            ((lift (M := fun (i : ι) ↦ FreeGroup Unit) :
                (a : (i : ι) → FreeGroup Unit →* G) → (CoprodI fun (i : ι) ↦ FreeGroup Unit) →* G)
              fun (i : ι) ↦ (FreeGroup.lift : (a : Unit → G) → FreeGroup Unit →* G) fun (x : Unit) ↦ a i)
            (MulEquiv.toMonoidHom freeGroupEquivCoprodI) :
          (a : FreeGroup ι) → G)
        (FreeGroup.of i) :
      G)
Tactic: ext i
-- 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
⊢ Function.Injective (α := FreeGroup ι) (β := G)
    (⇑((FreeGroup.lift : (a : ι → G) → FreeGroup ι →* G) a : FreeGroup ι →* G) : (a : FreeGroup ι) → G)
have this : Eq (α := FreeGroup ι →* G) ((FreeGroup.lift : (a : ι → G) → FreeGroup ι →* G) a : FreeGroup ι →* G)
  (MonoidHom.comp
      ((lift (M := fun (i : ι) ↦ FreeGroup Unit) :
          (a : (i : ι) → FreeGroup Unit →* G) → (CoprodI fun (i : ι) ↦ FreeGroup Unit) →* G)
        fun (i : ι) ↦ (FreeGroup.lift : (a : Unit → G) → FreeGroup Unit →* G) fun (x : Unit) ↦ a i)
      (MulEquiv.toMonoidHom freeGroupEquivCoprodI) :
    FreeGroup ι →* G)
Tactic: have : FreeGroup.lift a =
      (CoprodI.lift fun i => FreeGroup.lift fun _ => a i).comp
        (@freeGroupEquivCoprodI ι).toMonoidHom := by
    ext i
    simp
-- 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
this :
  Eq (α := FreeGroup ι →* G) ((FreeGroup.lift : (a : ι → G) → FreeGroup ι →* G) a : FreeGroup ι →* G)
    (MonoidHom.comp
        ((lift (M := fun (i : ι) ↦ FreeGroup Unit) :
            (a : (i : ι) → FreeGroup Unit →* G) → (CoprodI fun (i : ι) ↦ FreeGroup Unit) →* G)
          fun (i : ι) ↦ (FreeGroup.lift : (a : Unit → G) → FreeGroup Unit →* G) fun (x : Unit) ↦ a i)
        (MulEquiv.toMonoidHom freeGroupEquivCoprodI) :
      FreeGroup ι →* G)
⊢ Function.Injective (α := FreeGroup ι) (β := G)
    (⇑((FreeGroup.lift : (a : ι → G) → FreeGroup ι →* G) a : FreeGroup ι →* G) : (a : FreeGroup ι) → G)
have rw : Function.Injective.{u_1 + 1, u_1 + 1} (α := FreeGroup ι) (β := G)
  (Function.comp (β := CoprodI fun (i : ι) ↦ FreeGroup Unit)
    (⇑((lift (M := fun (i : ι) ↦ FreeGroup Unit) :
            (a : (i : ι) → FreeGroup Unit →* G) → (CoprodI fun (i : ι) ↦ FreeGroup Unit) →* G)
          fun (i : ι) ↦ (FreeGroup.lift : (a : Unit → G) → FreeGroup Unit →* G) fun (x : Unit) ↦ a i) :
      (a : CoprodI fun (i : ι) ↦ FreeGroup Unit) → G)
    (⇑(MulEquiv.toMonoidHom freeGroupEquivCoprodI) : (a : FreeGroup ι) → CoprodI fun (i : ι) ↦ FreeGroup Unit))
Tactic: rw [this, MonoidHom.coe_comp]
-- 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
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := FreeGroup ι) (β := G)
    (Function.comp (β := CoprodI fun (i : ι) ↦ FreeGroup Unit)
      (⇑((lift (M := fun (i : ι) ↦ FreeGroup Unit) :
              (a : (i : ι) → FreeGroup Unit →* G) → (CoprodI fun (i : ι) ↦ FreeGroup Unit) →* G)
            fun (i : ι) ↦ (FreeGroup.lift : (a : Unit → G) → FreeGroup Unit →* G) fun (x : Unit) ↦ a i) :
        (a : CoprodI fun (i : ι) ↦ FreeGroup Unit) → G)
      (⇑(MulEquiv.toMonoidHom freeGroupEquivCoprodI) : (a : FreeGroup ι) → CoprodI fun (i : ι) ↦ FreeGroup Unit))
have refine : Function.Injective.{u_1 + 1, u_1 + 1} (α := CoprodI fun (i : ι) ↦ FreeGroup Unit) (β := G)
  (⇑((lift (M := fun (i : ι) ↦ FreeGroup Unit) :
          (a : (i : ι) → FreeGroup Unit →* G) → (CoprodI fun (i : ι) ↦ FreeGroup Unit) →* G)
        fun (i : ι) ↦ (FreeGroup.lift : (a : Unit → G) → FreeGroup Unit →* G) fun (x : Unit) ↦ a i) :
    (a : CoprodI fun (i : ι) ↦ FreeGroup Unit) → G)
Tactic: refine Function.Injective.comp ?_ (MulEquiv.injective freeGroupEquivCoprodI)
-- 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
⊢ Function.Injective.{max (u_1 + 1) 1, u_1 + 1} (α := CoprodI fun (i : ι) ↦ FreeGroup Unit) (β := G)
    (⇑((lift (M := fun (i : ι) ↦ FreeGroup Unit) :
            (a : (i : ι) → FreeGroup Unit →* G) → (CoprodI fun (i : ι) ↦ FreeGroup Unit) →* G)
          fun (i : ι) ↦ (FreeGroup.lift : (a : Unit → G) → FreeGroup Unit →* G) fun (x : Unit) ↦ a i) :
      (a : CoprodI fun (i : ι) ↦ FreeGroup Unit) → G)
have hXnonempty₁ : ∀ (i : ι), (X' i).Nonempty
Tactic: apply lift_injective_of_ping_pong f _ X'
-- 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
hXnonempty₁ : ∀ (i : ι), (X' i).Nonempty
⊢ Function.Injective.{max (u_1 + 1) 1, u_1 + 1} (α := CoprodI fun (i : ι) ↦ FreeGroup Unit) (β := G)
    (⇑((lift (M := fun (i : ι) ↦ FreeGroup Unit) :
            (a : (i : ι) → FreeGroup Unit →* G) → (CoprodI fun (i : ι) ↦ FreeGroup Unit) →* G)
          fun (i : ι) ↦ (FreeGroup.lift : (a : Unit → G) → FreeGroup Unit →* G) fun (x : Unit) ↦ a i) :
      (a : CoprodI fun (i : ι) ↦ FreeGroup Unit) → G)
have hXdisj₁ : Pairwise (Disjoint on X')
Tactic: apply lift_injective_of_ping_pong f _ X'
-- 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
hXnonempty₁ : ∀ (i : ι), (X' i).Nonempty
hXdisj₁ : Pairwise (Disjoint on X')
⊢ Function.Injective.{max (u_1 + 1) 1, u_1 + 1} (α := CoprodI fun (i : ι) ↦ FreeGroup Unit) (β := G)
    (⇑((lift (M := fun (i : ι) ↦ FreeGroup Unit) :
            (a : (i : ι) → FreeGroup Unit →* G) → (CoprodI fun (i : ι) ↦ FreeGroup Unit) →* G)
          fun (i : ι) ↦ (FreeGroup.lift : (a : Unit → G) → FreeGroup Unit →* G) fun (x : Unit) ↦ a i) :
      (a : CoprodI fun (i : ι) ↦ FreeGroup Unit) → G)
have 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
Tactic: apply lift_injective_of_ping_pong f _ X'
-- 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
hXnonempty₁ : ∀ (i : ι), (X' i).Nonempty
hXdisj₁ : Pairwise (Disjoint on X')
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
⊢ Function.Injective.{max (u_1 + 1) 1, u_1 + 1} (α := CoprodI fun (i : ι) ↦ FreeGroup Unit) (β := G)
    (⇑((lift (M := fun (i : ι) ↦ FreeGroup Unit) :
            (a : (i : ι) → FreeGroup Unit →* G) → (CoprodI fun (i : ι) ↦ FreeGroup Unit) →* G)
          fun (i : ι) ↦ (FreeGroup.lift : (a : Unit → G) → FreeGroup Unit →* G) fun (x : Unit) ↦ a i) :
      (a : CoprodI fun (i : ι) ↦ FreeGroup Unit) → G)
have apply : 3 ≤ #ι ∨ ∃ (i : ι), 3 ≤ #(H i)
Tactic: apply lift_injective_of_ping_pong f _ X'
-- 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
⊢ Function.onFun.{u_1 + 1, u_4 + 1, 1} (β := Set α) Disjoint (fun (i : ι) ↦ X i ∪ Y i) i j
have hXdisj₁ : Disjoint (X i) ((fun (i : ι) ↦ X i ∪ Y i) j)
Tactic: apply Disjoint.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
hXdisj₁ : Disjoint (X i) ((fun (i : ι) ↦ X i ∪ Y i) j)
⊢ Function.onFun.{u_1 + 1, u_4 + 1, 1} (β := Set α) Disjoint (fun (i : ι) ↦ X i ∪ Y i) i j
have hXdisj₂ : Disjoint (Y i) ((fun (i : ι) ↦ X i ∪ Y i) j)
Tactic: apply Disjoint.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
⊢ Disjoint (X i) ((fun (i : ι) ↦ X i ∪ Y i) j)
have hXdisj₁ : Disjoint (X i) (X j)
Tactic: apply Disjoint.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
i j : ι
hij : i ≠ j
hXdisj₁ : Disjoint (X i) (X j)
⊢ Disjoint (X i) ((fun (i : ι) ↦ X i ∪ Y i) j)
have hXdisj₂ : Disjoint (X i) (Y j)
Tactic: apply Disjoint.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
i j : ι
hij : i ≠ j
⊢ Disjoint (Y i) ((fun (i : ι) ↦ X i ∪ Y i) j)
have hXdisj₁ : Disjoint (Y i) (X j)
Tactic: apply Disjoint.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
i j : ι
hij : i ≠ j
hXdisj₁ : Disjoint (Y i) (X j)
⊢ Disjoint (Y i) ((fun (i : ι) ↦ X i ∪ Y i) j)
have hXdisj₂ : Disjoint (Y i) (Y j)
Tactic: apply Disjoint.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
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
have 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
Tactic: refine FreeGroup.freeGroupUnitEquivInt.forall_congr_left.mpr ?_
-- 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 : ℤ
hne1 : Ne (α := H i) ((FreeGroup.freeGroupUnitEquivInt.symm : (a : ℤ) → FreeGroup Unit) n : FreeGroup Unit) (1 : H i)
⊢ HSMul.hSMul (α := G)
      ((f i : (a : H i) → G) ((FreeGroup.freeGroupUnitEquivInt.symm : (a : ℤ) → FreeGroup Unit) n : FreeGroup Unit) : G)
      (X' j) ⊆
    X' i
have 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
Tactic: change FreeGroup.lift (fun _ => a i) (FreeGroup.of () ^ n) • X' j ⊆ X' i
-- 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 : ℤ
hne1 : Ne (α := H i) ((FreeGroup.freeGroupUnitEquivInt.symm : (a : ℤ) → FreeGroup Unit) n : FreeGroup Unit) (1 : H 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
have hpp : a i ^ n • X' j ⊆ X' i
Tactic: simp only [map_zpow, FreeGroup.lift_apply_of]
-- 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
hne1 : Ne (α := H i) ((FreeGroup.freeGroupUnitEquivInt.symm : (a : ℤ) → FreeGroup Unit) 0) 1
⊢ False
have apply : Eq (α := H i) ((FreeGroup.freeGroupUnitEquivInt.symm : (a : ℤ) → FreeGroup Unit) 0) 1
Tactic: apply hne1
-- 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 : ℤ
hne1 : Ne (α := H i) ((FreeGroup.freeGroupUnitEquivInt.symm : (a : ℤ) → FreeGroup Unit) n : FreeGroup Unit) (1 : H i)
⊢ a i ^ n • X' j ⊆ X' i
have hnne0 : n ≠ 0
Tactic: have hnne0 : n ≠ 0 := by
      rintro rfl
      apply hne1
      simp [H, FreeGroup.freeGroupUnitEquivInt]
-- 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
⊢ a i ^ n • (X j ∪ Y j) ⊆ X i ∪ Y i
have hpp : ∀ (hlt : 0 < n), a i ^ n • (X j ∪ Y j) ⊆ X i ∪ Y i
Tactic: rcases (lt_or_gt_of_ne hnne0).symm with hlt | hgt