awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.CoprodI
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
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)
⊢ 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))

Tactic:
ext i a
-- Module: Mathlib.GroupTheory.CoprodI
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
i : ι
⊢ 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 PUnit.unit) :
      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 PUnit.unit) :
      CoprodI fun (x : ι) ↦ FreeGroup Unit)

Tactic:
simp
-- 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 :
  ∀ (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)
⊢ 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:
ext 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
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:
simp
-- 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
⊢ 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
-- 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
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)
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))
⊢ Function.Injective (α := FreeGroup ι) (β := G)
    (⇑((FreeGroup.lift : (a : ι → G) → FreeGroup ι →* G) a : FreeGroup ι →* G) : (a : FreeGroup ι) → G)

Tactic:
rw [this, MonoidHom.coe_comp]

Premises used: MonoidHom.coe_comp
-- 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
⊢ 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:
Function.Injective.comp ?_ (MulEquiv.injective freeGroupEquivCoprodI)

Premises used: freeGroupEquivCoprodI, Function.Injective.comp, MulEquiv.injective
-- 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
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)
⊢ 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:
refine Function.Injective.comp ?_ (MulEquiv.injective freeGroupEquivCoprodI)

Premises used: freeGroupEquivCoprodI, Function.Injective.comp, MulEquiv.injective
-- 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
change :
  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)
⊢ 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:
change Function.Injective (lift fun i : ι => FreeGroup.lift fun _ => a i)

Premises used: Monoid.CoprodI.lift, FreeGroup.lift, Function.Injective, 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
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
apply : 3 ≤ #ι ∨ ∃ (i : ι), 3 ≤ #(H 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)

Tactic:
apply lift_injective_of_ping_pong f _ X'

Premises used: Monoid.CoprodI.lift_injective_of_ping_pong
-- 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 : ι), (X' i).Nonempty

Tactic:
fun i => Set.Nonempty.inl (hXnonempty i)

Premises used: Set.Nonempty.inl
-- 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 : ι), (X' i).Nonempty

Tactic:
exact fun i => Set.Nonempty.inl (hXnonempty i)

Premises used: Set.Nonempty.inl
-- 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
hXdisj₁ : Function.onFun.{u_1 + 1, u_4 + 1, 1} (β := Set α) Disjoint (fun (i : ι) ↦ X i ∪ Y i) i j
⊢ (Disjoint on X') i j

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
hXdisj₁ : Disjoint (X i) ((fun (i : ι) ↦ X i ∪ Y i) j)
hXdisj₂ : Disjoint (Y 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

Tactic:
apply Disjoint.union_left

Premises used: 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
hXdisj₁ : Disjoint (X i) (X j)
hXdisj₂ : Disjoint (X i) (Y j)
⊢ Disjoint (X i) ((fun (i : ι) ↦ X i ∪ Y i) j)

Tactic:
apply Disjoint.union_right

Premises used: Disjoint.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
hXdisj₁ : Disjoint (Y i) (X j)
hXdisj₂ : Disjoint (Y i) (Y j)
⊢ Disjoint (Y i) ((fun (i : ι) ↦ X i ∪ Y i) j)

Tactic:
apply Disjoint.union_right

Premises used: Disjoint.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
⊢ Disjoint (X i) (X j)

Tactic:
hXdisj 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 (X i) (X j)

Tactic:
exact hXdisj 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 (X i) (Y j)

Tactic:
hXYdisj i j
-- 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 (X i) (Y j)

Tactic:
exact hXYdisj i j
-- 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) (X j)

Tactic:
(hXYdisj j i).symm

Premises used: 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
⊢ Disjoint (Y i) (X j)

Tactic:
exact (hXYdisj j i).symm

Premises used: Disjoint.symm