awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ≤ #ι
⊢ 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 : ∀ (i_1 : ι) (h1 : i_1 ≠ i) (h2 : i_1 ≠ 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)
Tactic: obtain ⟨i, h1, h2⟩ := Cardinal.exists_ne_ne_of_three_le hcard i j
-- 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 : ∃ (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)
have inr : ∀ (k : ι) (hcard : 3 ≤ #(H k)),
  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, 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
α : 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
k : ι
hcard : 3 ≤ #(H k)
⊢ 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 pos : ∀ (hh : i = k),
  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: by_cases hh : i = 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 j : ι
w : NeWord H i j
k : ι
hcard : 3 ≤ #(H k)
pos :
  ∀ (hh : i = k),
    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 neg : ∀ (hh : ¬i = k),
  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: by_cases hh : i = 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 j : ι
w : NeWord H i j
k : ι
hcard : 3 ≤ #(H k)
hh : i = k
⊢ 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 pos : ∀ (hl : j = k),
  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: by_cases hl : j = 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 j : ι
w : NeWord H i j
k : ι
hcard : 3 ≤ #(H k)
hh : i = k
pos :
  ∀ (hl : j = k),
    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 neg : ∀ (hl : ¬j = k),
  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: by_cases hl : j = 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 j : ι
w : NeWord H i j
k : ι
hcard : 3 ≤ #(H k)
hh : ¬i = k
⊢ 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 pos : ∀ (hl : j = k),
  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: by_cases hl : j = 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 j : ι
w : NeWord H i j
k : ι
hcard : 3 ≤ #(H k)
hh : ¬i = k
pos :
  ∀ (hl : j = k),
    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 neg : ∀ (hl : ¬j = k),
  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: by_cases hl : j = k
-- 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
k : ι
hcard : 3 ≤ #(H k)
hh : i = k
hl : j = k
⊢ 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 hcard₁ : 3 ≤ #(H i)
Tactic: subst hh
Cleared hypotheses: k, hcard, hh, hl
-- 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
k : ι
hcard : 3 ≤ #(H k)
hh : i = k
hl : j = k
hcard₁ : 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)
have hl₁ : j = i
Tactic: subst hh
Cleared hypotheses: k, hcard, hh, hl
-- 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)
hl : j = 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 pos : ∀ (w : NeWord H j j) (hcard : 3 ≤ #(H 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)
Tactic: subst hl
Cleared hypotheses: i, w, hcard, hl
-- 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
k : ι
hcard : 3 ≤ #(H k)
hh : i = k
hl : ¬j = k
⊢ 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 hcard₁ : 3 ≤ #(H i)
Tactic: subst hh
Cleared hypotheses: k, hcard, hh, hl
-- 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
k : ι
hcard : 3 ≤ #(H k)
hh : i = k
hl : ¬j = k
hcard₁ : 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)
have hl₁ : ¬j = i
Tactic: subst hh
Cleared hypotheses: k, hcard, hh, hl
-- 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)
hl : ¬j = 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 hl₁ : j ≠ i
Tactic: change j ≠ i at hl
Cleared hypotheses: hl
-- 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
k : ι
hcard : 3 ≤ #(H k)
hh : ¬i = k
hl : j = k
⊢ 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 hcard₁ : 3 ≤ #(H j)
Tactic: subst hl
Cleared hypotheses: k, hcard, hh, hl
-- 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
k : ι
hcard : 3 ≤ #(H k)
hh : ¬i = k
hl : j = k
hcard₁ : 3 ≤ #(H 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 hh₁ : ¬i = j
Tactic: subst hl
Cleared hypotheses: k, hcard, hh, hl
-- 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 j)
hh : ¬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 hh₁ : i ≠ j
Tactic: change i ≠ j at hh
Cleared hypotheses: hh
-- 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 j)
hh : 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 this : 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.inv (G := H).prod (M := H)) :
    G)
  (1 : G)
Tactic: have : lift f w.inv.prod ≠ 1 :=
          lift_word_prod_nontrivial_of_head_card f X hXnonempty hXdisj hpp w.inv hcard hh.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
inst_3 : Nontrivial ι
i j : ι
w : NeWord H i j
hcard : 3 ≤ #(H j)
hh : i ≠ j
this :
  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.inv (G := H).prod (M := H)) :
      G)
    (1 : G)
heq :
  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 pos : 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.inv (G := H).prod (M := H)) :
    G)
  (1 : G)
Tactic: apply this
-- 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
k : ι
hcard : 3 ≤ #(H k)
hh : ¬i = k
hl : ¬j = k
⊢ 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 hh₁ : i ≠ k
Tactic: change i ≠ k at hh
Cleared hypotheses: hh
-- 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
k : ι
hcard : 3 ≤ #(H k)
hl : ¬j = k
hh : i ≠ k
⊢ 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 hl₁ : j ≠ k
Tactic: change j ≠ k at hl
Cleared hypotheses: hl
-- 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: classical
    rcases hcard with hcard | hcard
    · obtain ⟨i, h1, h2⟩ := Cardinal.exists_ne_ne_of_three_le hcard i j
      exact lift_word_prod_nontrivial_of_other_i f X hXnonempty hXdisj hpp w h1 h2
    · obtain ⟨k, hcard⟩ := hcard
      by_cases hh : i = k <;> by_cases hl : j = k
      · subst hh
        subst hl
        exact lift_word_prod_nontrivial_of_head_eq_last f X hXnonempty hXdisj hpp w
      · subst hh
        change j ≠ i at hl
        exact lift_word_prod_nontrivial_of_head_card f X hXnonempty hXdisj hpp w hcard hl.symm
      · subst hl
        change i ≠ j at hh
        have : lift f w.inv.prod ≠ 1 :=
          lift_word_prod_nontrivial_of_head_card f X hXnonempty hXdisj hpp w.inv hcard hh.symm
        intro heq
        apply this
        simpa using heq
      · change i ≠ k at hh
        change j ≠ k at hl
        exact lift_word_prod_nontrivial_of_other_i f X hXnonempty hXdisj hpp w hh.symm hl.symm
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: classical
    rcases hcard with hcard | hcard
    · obtain ⟨i, h1, h2⟩ := Cardinal.exists_ne_ne_of_three_le hcard i j
      exact lift_word_prod_nontrivial_of_other_i f X hXnonempty hXdisj hpp w h1 h2
    · obtain ⟨k, hcard⟩ := hcard
      by_cases hh : i = k <;> by_cases hl : j = k
      · subst hh
        subst hl
        exact lift_word_prod_nontrivial_of_head_eq_last f X hXnonempty hXdisj hpp w
      · subst hh
        change j ≠ i at hl
        exact lift_word_prod_nontrivial_of_head_card f X hXnonempty hXdisj hpp w hcard hl.symm
      · subst hl
        change i ≠ j at hh
        have : lift f w.inv.prod ≠ 1 :=
          lift_word_prod_nontrivial_of_head_card f X hXnonempty hXdisj hpp w.inv hcard hh.symm
        intro heq
        apply this
        simpa using heq
      · change i ≠ k at hh
        change j ≠ k at hl
        exact lift_word_prod_nontrivial_of_other_i f X hXnonempty hXdisj hpp w hh.symm hl.symm
Cleared hypotheses: hcard