awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
i j i_1 j_1 k l : ι
_w₁ : NeWord M i_1 j_1
_hne : j_1 ≠ k
_w₂ : NeWord M k l
w_ih_w₂ :
  ∀ (x : M k) (hnotone : x * _w₂.head (M := M) ≠ 1),
    (replaceHead (M := M) (x * _w₂.head (M := M)) hnotone _w₂).prod (M := M) =
      HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M k) → CoprodI M) x : CoprodI M) (_w₂.prod (M := M))
x : M i_1
hnotone : x * (_w₁.append (M := M) _hne _w₂).head (M := M) ≠ 1
w_ih_w₁ :
  (replaceHead (M := M) (x * _w₁.head (M := M)) hnotone _w₁).prod (M := M) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i_1) → CoprodI M) x : CoprodI M) (_w₁.prod (M := M))
⊢ (replaceHead (M := M) (x * (_w₁.append (M := M) _hne _w₂).head (M := M)) hnotone (_w₁.append (M := M) _hne _w₂)).prod
      (M := M) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i_1) → CoprodI M) x : CoprodI M)
      ((_w₁.append (M := M) _hne _w₂).prod (M := M))
have append : (replaceHead (M := M) (x * (_w₁.append (M := M) _hne _w₂).head (M := M)) hnotone _w₁).prod (M := M) *
    _w₂.prod (M := M) =
  HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i_1) → CoprodI M) x : CoprodI M) (_w₁.prod (M := M)) *
    _w₂.prod (M := M)
Tactic: simp only [replaceHead, append_prod, ← mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
i j : ι
w : NeWord M i j
x : M i
hnotone : x * w.head (M := M) ≠ 1
⊢ (replaceHead (M := M) (x * w.head (M := M)) hnotone w).prod (M := M) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) x : CoprodI M) (w.prod (M := M))
have singleton : ∀ {i : ι} (x : M i) (a : x ≠ 1) (x_1 : M i) (hnotone : x_1 * (singleton (M := M) x a).head (M := M) ≠ 1),
  (replaceHead (M := M) (x_1 * (singleton (M := M) x a).head (M := M)) hnotone (singleton (M := M) x a)).prod (M := M) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) x_1 : CoprodI M)
      ((singleton (M := M) x a).prod (M := M))
Tactic: induction w with
  | singleton => simp [replaceHead]
  | append _ _ _ w_ih_w₁ w_ih_w₂ =>
    specialize w_ih_w₁ _ hnotone
    simp only [replaceHead, append_prod, ← mul_assoc]
    congr 1
Cleared hypotheses: w, x, hnotone
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
i j : ι
w : NeWord M i j
x : M i
hnotone : x * w.head (M := M) ≠ 1
singleton :
  ∀ {i : ι} (x : M i) (a : x ≠ 1) (x_1 : M i) (hnotone : x_1 * (NeWord.singleton (M := M) x a).head (M := M) ≠ 1),
    (replaceHead (M := M) (x_1 * (NeWord.singleton (M := M) x a).head (M := M)) hnotone
            (NeWord.singleton (M := M) x a)).prod
        (M := M) =
      HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) x_1 : CoprodI M)
        ((NeWord.singleton (M := M) x a).prod (M := M))
⊢ (replaceHead (M := M) (x * w.head (M := M)) hnotone w).prod (M := M) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) x : CoprodI M) (w.prod (M := M))
have append : ∀ {i j k l : ι} (_w₁ : NeWord M i j) (_hne : j ≠ k) (_w₂ : NeWord M k l)
  (w_ih_w₁ :
    ∀ (x : M i) (hnotone : x * _w₁.head (M := M) ≠ 1),
      (replaceHead (M := M) (x * _w₁.head (M := M)) hnotone _w₁).prod (M := M) =
        HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) x : CoprodI M) (_w₁.prod (M := M)))
  (w_ih_w₂ :
    ∀ (x : M k) (hnotone : x * _w₂.head (M := M) ≠ 1),
      (replaceHead (M := M) (x * _w₂.head (M := M)) hnotone _w₂).prod (M := M) =
        HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M k) → CoprodI M) x : CoprodI M) (_w₂.prod (M := M)))
  (x : M i) (hnotone : x * (_w₁.append (M := M) _hne _w₂).head (M := M) ≠ 1),
  (replaceHead (M := M) (x * (_w₁.append (M := M) _hne _w₂).head (M := M)) hnotone (_w₁.append (M := M) _hne _w₂)).prod
      (M := M) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) x : CoprodI M)
      ((_w₁.append (M := M) _hne _w₂).prod (M := M))
Tactic: induction w with
  | singleton => simp [replaceHead]
  | append _ _ _ w_ih_w₁ w_ih_w₂ =>
    specialize w_ih_w₁ _ hnotone
    simp only [replaceHead, append_prod, ← mul_assoc]
    congr 1
Cleared hypotheses: w, x, hnotone
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
G : ι → Type u_4
inst : (i : ι) → Group (G i)
i j : ι
w : NeWord G i j
⊢ w.inv (G := G).prod (M := G) = (w.prod (M := G))⁻¹
have singleton : ∀ {i : ι} (x : G i) (a : x ≠ 1),
  Eq (α := CoprodI G) (prod (M := G) (inv (G := G) (singleton (M := G) x a))) (prod (M := G) (singleton (M := G) x a))⁻¹
Tactic: induction w
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
G : ι → Type u_4
inst : (i : ι) → Group (G i)
i j : ι
w : NeWord G i j
singleton :
  ∀ {i : ι} (x : G i) (a : x ≠ 1),
    Eq (α := CoprodI G) (prod (M := G) (inv (G := G) (NeWord.singleton (M := G) x a)))
      (prod (M := G) (NeWord.singleton (M := G) x a))⁻¹
⊢ w.inv (G := G).prod (M := G) = (w.prod (M := G))⁻¹
have append : ∀ {i j k l : ι} (_w₁ : NeWord G i j) (_hne : j ≠ k) (_w₂ : NeWord G k l),
  _w₁.inv (G := G).prod (M := G) = (_w₁.prod (M := G))⁻¹ →
    _w₂.inv (G := G).prod (M := G) = (_w₂.prod (M := G))⁻¹ →
      (_w₁.append (M := G) _hne _w₂).inv (G := G).prod (M := G) = ((_w₁.append (M := G) _hne _w₂).prod (M := G))⁻¹
Tactic: induction w
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
G : ι → Type u_4
inst : (i : ι) → Group (G i)
i j : ι
w : NeWord G i j
⊢ w.inv (G := G).head (M := G) = (w.last (M := G))⁻¹
have singleton : ∀ {i : ι} (x : G i) (a : x ≠ 1),
  head (M := G) (inv (G := G) (singleton (M := G) x a)) = (last (M := G) (singleton (M := G) x a))⁻¹
Tactic: induction w
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
G : ι → Type u_4
inst : (i : ι) → Group (G i)
i j : ι
w : NeWord G i j
singleton :
  ∀ {i : ι} (x : G i) (a : x ≠ 1),
    head (M := G) (inv (G := G) (NeWord.singleton (M := G) x a)) = (last (M := G) (NeWord.singleton (M := G) x a))⁻¹
⊢ w.inv (G := G).head (M := G) = (w.last (M := G))⁻¹
have append : ∀ {i j k l : ι} (_w₁ : NeWord G i j) (_hne : j ≠ k) (_w₂ : NeWord G k l),
  _w₁.inv (G := G).head (M := G) = (_w₁.last (M := G))⁻¹ →
    _w₂.inv (G := G).head (M := G) = (_w₂.last (M := G))⁻¹ →
      (_w₁.append (M := G) _hne _w₂).inv (G := G).head (M := G) = ((_w₁.append (M := G) _hne _w₂).last (M := G))⁻¹
Tactic: induction w
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
G : ι → Type u_4
inst : (i : ι) → Group (G i)
i j : ι
w : NeWord G i j
⊢ w.inv (G := G).last (M := G) = (w.head (M := G))⁻¹
have singleton : ∀ {i : ι} (x : G i) (a : x ≠ 1),
  last (M := G) (inv (G := G) (singleton (M := G) x a)) = (head (M := G) (singleton (M := G) x a))⁻¹
Tactic: induction w
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
G : ι → Type u_4
inst : (i : ι) → Group (G i)
i j : ι
w : NeWord G i j
singleton :
  ∀ {i : ι} (x : G i) (a : x ≠ 1),
    last (M := G) (inv (G := G) (NeWord.singleton (M := G) x a)) = (head (M := G) (NeWord.singleton (M := G) x a))⁻¹
⊢ w.inv (G := G).last (M := G) = (w.head (M := G))⁻¹
have append : ∀ {i j k l : ι} (_w₁ : NeWord G i j) (_hne : j ≠ k) (_w₂ : NeWord G k l),
  _w₁.inv (G := G).last (M := G) = (_w₁.head (M := G))⁻¹ →
    _w₂.inv (G := G).last (M := G) = (_w₂.head (M := G))⁻¹ →
      (_w₁.append (M := G) _hne _w₂).inv (G := G).last (M := G) = ((_w₁.append (M := G) _hne _w₂).head (M := G))⁻¹
Tactic: induction w
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
i_1 j_1 i j k_1 l : ι
w₁ : NeWord H i j
hne : j ≠ k_1
w₂ : NeWord H k_1 l
hIw₁ :
  ∀ {k : ι} (hk : j ≠ k),
    HSMul.hSMul.{u_4, u_6, u_6} (α := G)
        ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
            (w₁.prod (M := H)) :
          G)
        (X k) ⊆
      X i
hIw₂ :
  ∀ {k : ι} (hk : l ≠ k),
    HSMul.hSMul.{u_4, u_6, u_6} (α := G)
        ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
            (w₂.prod (M := H)) :
          G)
        (X k) ⊆
      X k_1
k : ι
hk : l ≠ k
⊢ HSMul.hSMul.{u_4, u_6, u_6} (α := G)
      ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
          ((w₁.append (M := H) hne w₂).prod (M := H)) :
        G)
      (X k) ⊆
    X i
have lift : HSMul.hSMul.{u_4, u_6, u_6} (α := G)
    ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
        ((w₁.append (M := H) hne w₂).prod (M := H)) :
      G)
    (X k) =
  HSMul.hSMul.{u_4, u_6, u_6} (α := G)
    ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
        (w₁.prod (M := H)) :
      G)
    (HSMul.hSMul.{u_4, u_6, u_6} (α := G)
      ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
          (w₂.prod (M := H)) :
        G)
      (X k))
Tactic: calc
      lift f (NeWord.append w₁ hne w₂).prod • X k = lift f w₁.prod • lift f w₂.prod • X k := by
        simp [mul_smul]
      _ ⊆ lift f w₁.prod • X _ := smul_set_subset_smul_set_iff.mpr (hIw₂ hk)
      _ ⊆ X i := hIw₁ hne
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
i j k : ι
w : NeWord H i j
hk : j ≠ k
⊢ HSMul.hSMul.{u_4, u_6, u_6} (α := G)
      ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
          (w.prod (M := H)) :
        G)
      (X k) ⊆
    X i
have singleton : ∀ {i : ι} (x : H i) (hne_one : x ≠ 1) {k : ι} (hk : i ≠ k),
  HSMul.hSMul.{u_4, u_6, u_6} (α := G)
      ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
          (NeWord.prod (M := H) (NeWord.singleton (M := H) x hne_one)) :
        G)
      (X k) ⊆
    X i
Tactic: induction w generalizing k with
  | singleton x hne_one => simpa using hpp hk _ hne_one
  | @append i j k l w₁ hne w₂ hIw₁ hIw₂ =>
    calc
      lift f (NeWord.append w₁ hne w₂).prod • X k = lift f w₁.prod • lift f w₂.prod • X k := by
        simp [mul_smul]
      _ ⊆ lift f w₁.prod • X _ := smul_set_subset_smul_set_iff.mpr (hIw₂ hk)
      _ ⊆ X i := hIw₁ hne
Cleared hypotheses: k, w, hk
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
i j k : ι
w : NeWord H i j
hk : j ≠ k
singleton :
  ∀ {i : ι} (x : H i) (hne_one : x ≠ 1) {k : ι} (hk : i ≠ k),
    HSMul.hSMul.{u_4, u_6, u_6} (α := G)
        ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
            (NeWord.prod (M := H) (NeWord.singleton (M := H) x hne_one)) :
          G)
        (X k) ⊆
      X i
⊢ HSMul.hSMul.{u_4, u_6, u_6} (α := G)
      ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
          (w.prod (M := H)) :
        G)
      (X k) ⊆
    X i
have append : ∀ {i j k l : ι} (w₁ : NeWord H i j) (hne : j ≠ k) (w₂ : NeWord H k l)
  (hIw₁ :
    ∀ {k : ι} (hk : j ≠ k),
      HSMul.hSMul.{u_4, u_6, u_6} (α := G)
          ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
              (w₁.prod (M := H)) :
            G)
          (X k) ⊆
        X i)
  (hIw₂ :
    ∀ {k_1 : ι} (hk : l ≠ k_1),
      HSMul.hSMul.{u_4, u_6, u_6} (α := G)
          ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
              (w₂.prod (M := H)) :
            G)
          (X k_1) ⊆
        X k)
  {k_1 : ι} (hk : l ≠ k_1),
  HSMul.hSMul.{u_4, u_6, u_6} (α := G)
      ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
          ((w₁.append (M := H) hne w₂).prod (M := H)) :
        G)
      (X k_1) ⊆
    X i
Tactic: induction w generalizing k with
  | singleton x hne_one => simpa using hpp hk _ hne_one
  | @append i j k l w₁ hne w₂ hIw₁ hIw₂ =>
    calc
      lift f (NeWord.append w₁ hne w₂).prod • X k = lift f w₁.prod • lift f w₂.prod • X k := by
        simp [mul_smul]
      _ ⊆ lift f w₁.prod • X _ := smul_set_subset_smul_set_iff.mpr (hIw₂ hk)
      _ ⊆ X i := hIw₁ hne
Cleared hypotheses: k, w, hk
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (hypothesis)
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
i j k : ι
w : NeWord H i j
hhead : k ≠ i
hlast : k ≠ j
heq1 :
  Eq.{u_4 + 1} (α := G)
    ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
        (w.prod (M := H)) :
      G)
    (1 : G)
⊢ False
have this : X k ⊆ X i
Tactic: have : X k ⊆ X i := by simpa [heq1] using lift_word_ping_pong f X hpp w hlast.symm
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
i j k : ι
w : NeWord H i j
hhead : k ≠ i
hlast : k ≠ j
heq1 :
  Eq.{u_4 + 1} (α := G)
    ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
        (w.prod (M := H)) :
      G)
    (1 : G)
this : X k ⊆ X i
⊢ False
have obtain : ∀ (x : α) (hx : x ∈ X k), False
Tactic: obtain ⟨x, hx⟩ := hXnonempty k
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
inst_3 : Nontrivial ι
i : ι
w : NeWord H i i
⊢ Ne.{u_4 + 1} (α := G)
    ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
        (w.prod (M := H)) :
      G)
    (1 : G)
have obtain : ∀ (k : ι) (hk : k ≠ i),
  Ne.{u_4 + 1} (α := G)
    ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
        (w.prod (M := H)) :
      G)
    (1 : G)
Tactic: obtain ⟨k, hk⟩ := exists_ne i
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
inst_3 : Nontrivial ι
i j : ι
w : NeWord H i j
hcard : 3 ≤ #(H i)
hheadtail : i ≠ j
⊢ Ne.{u_4 + 1} (α := G)
    ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
        (w.prod (M := H)) :
      G)
    (1 : G)
have obtain : ∀ (h : H i) (hn1 : h ≠ 1) (hnh : h ≠ (w.head (M := H))⁻¹),
  Ne.{u_4 + 1} (α := G)
    ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
        (w.prod (M := H)) :
      G)
    (1 : G)
Tactic: obtain ⟨h, hn1, hnh⟩ := Cardinal.exists_ne_ne_of_three_le hcard 1 w.head⁻¹
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
inst_3 : Nontrivial ι
i j : ι
w : NeWord H i j
hcard : 3 ≤ #(H i)
hheadtail : i ≠ j
h : H i
hn1 : h ≠ 1
hnh : h ≠ (w.head (M := H))⁻¹
⊢ h * w.head (M := H) ≠ 1
have rw : h / (w.head (M := H))⁻¹ ≠ 1
Tactic: rw [← div_inv_eq_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (hypothesis)
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
inst_3 : Nontrivial ι
i j : ι
w : NeWord H i j
hcard : 3 ≤ #(H i)
hheadtail : i ≠ j
h : H i
hn1 : h ≠ 1
hnh : h ≠ (w.head (M := H))⁻¹
⊢ Ne.{u_4 + 1} (α := G)
    ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
        (w.prod (M := H)) :
      G)
    (1 : G)
have hnot1 : h * w.head (M := H) ≠ 1
Tactic: have hnot1 : h * w.head ≠ 1 := by
    rw [← div_inv_eq_mul]
    exact div_ne_one_of_ne hnh
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (hypothesis)
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
inst_3 : Nontrivial ι
i j : ι
w : NeWord H i j
hcard : 3 ≤ #(H i)
hheadtail : i ≠ j
h : H i
hn1 : h ≠ 1
hnh : h ≠ (w.head (M := H))⁻¹
hnot1 : h * w.head (M := H) ≠ 1
w' : NeWord H i i := (w.mulHead (M := H) h hnot1).append (M := H) ⋯ (NeWord.singleton (M := H) h⁻¹ ⋯)
⊢ Ne.{u_4 + 1} (α := G)
    ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
        (w.prod (M := H)) :
      G)
    (1 : G)
have hw' : Ne.{u_4 + 1} (α := G)
  ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
      (w'.prod (M := H)) :
    G)
  (1 : G)
Tactic: have hw' : lift f w'.prod ≠ 1 :=
    lift_word_prod_nontrivial_of_head_eq_last f X hXnonempty hXdisj hpp w'
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
inst_3 : Nontrivial ι
i j : ι
w : NeWord H i j
hcard : 3 ≤ #(H i)
hheadtail : i ≠ j
h : H i
hn1 : h ≠ 1
hnh : h ≠ (w.head (M := H))⁻¹
hnot1 : h * w.head (M := H) ≠ 1
w' : NeWord H i i := (w.mulHead (M := H) h hnot1).append (M := H) ⋯ (NeWord.singleton (M := H) h⁻¹ ⋯)
hw' :
  Ne.{u_4 + 1} (α := G)
    ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
        (w'.prod (M := H)) :
      G)
    (1 : G)
heq1 :
  Eq.{u_4 + 1} (α := G)
    ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
        (w.prod (M := H)) :
      G)
    (1 : G)
⊢ False
have apply : Eq.{u_4 + 1} (α := G)
  ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
      (w'.prod (M := H)) :
    G)
  (1 : G)
Tactic: apply hw'
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
hcard : 3 ≤ #ι ∨ ∃ (i : ι), 3 ≤ #(H i)
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
inst_3 : Nontrivial ι
i j : ι
w : NeWord H i j
⊢ Ne.{u_4 + 1} (α := G)
    ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
        (w.prod (M := H)) :
      G)
    (1 : G)
have inl : ∀ (hcard : 3 ≤ #ι),
  Ne.{u_4 + 1} (α := G)
    ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
        (w.prod (M := H)) :
      G)
    (1 : G)
Tactic: rcases hcard with hcard | hcard
Cleared hypotheses: hcard
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
hcard : 3 ≤ #ι ∨ ∃ (i : ι), 3 ≤ #(H i)
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
inst_3 : Nontrivial ι
i j : ι
w : NeWord H i j
inl :
  ∀ (hcard : 3 ≤ #ι),
    Ne.{u_4 + 1} (α := G)
      ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
          (w.prod (M := H)) :
        G)
      (1 : G)
⊢ Ne.{u_4 + 1} (α := G)
    ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
        (w.prod (M := H)) :
      G)
    (1 : G)
have inr : ∀ (hcard : ∃ (i : ι), 3 ≤ #(H i)),
  Ne.{u_4 + 1} (α := G)
    ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
        (w.prod (M := H)) :
      G)
    (1 : G)
Tactic: rcases hcard with hcard | hcard
Cleared hypotheses: hcard