awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
G : ι → Type u_4
inst_2 : (i : ι) → Group (G i)
m : ι
ih : G m
of :
  Eq (α := CoprodI G)
    ((CoprodI.of (M := G) : (a : G ⟨m, ih⟩.fst) → CoprodI G)
        (((Sigma.mk (β := fun (i : ι) ↦ G i) m ih).snd (β := fun (i : ι) ↦ G i))⁻¹ * ih) :
      CoprodI G)
    (1 : CoprodI G)
of₁ : Eq (α := CoprodI G) ((CoprodI.of (M := G) : (a : G ⟨m, ih⟩.fst) → CoprodI G) 1) 1
of₂ of₃ : Eq (α := CoprodI G) 1 1
⊢ HMul.hMul (α := CoprodI G) (β := CoprodI G)
      ((CoprodI.of (M := G) : (a : G ⟨m, ih⟩.fst) → CoprodI G)
          ((Sigma.mk (β := fun (i : ι) ↦ G i) m ih).snd (β := fun (i : ι) ↦ G i))⁻¹ :
        CoprodI G)
      ((CoprodI.of (M := G) : (a : G m) → CoprodI G) ih : CoprodI G) =
    1

Tactic:
rw [← of.map_mul, inv_mul_cancel, of.map_one]

Premises used: Monoid.CoprodI.of, inv_mul_cancel, MonoidHom.map_one, MonoidHom.map_mul
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : ι → Type u_4
inst : (i : ι) → Group (G i)
N : Type u_5
inst_1 : Group N
f : (i : ι) → MonoidHom.{u_4, u_5} (G i) N
s : Subgroup N
h : ∀ (i : ι), (f i).range ≤ s
⊢ Membership.mem (α := N) s
    ((((lift (M := G) : (a : (i : ι) → G i →* N) → CoprodI G →* N) f : CoprodI G →* N) : (a : CoprodI G) → N) 1 : N)

Tactic:
s.one_mem

Premises used: FreeMonoid.prodAux, Quotient.liftOn', Set.Mem, Subgroup.one_mem, Con.liftOn
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : ι → Type u_4
inst : (i : ι) → Group (G i)
N : Type u_5
inst_1 : Group N
f : (i : ι) → MonoidHom.{u_4, u_5} (G i) N
s : Subgroup N
h : ∀ (i : ι), (f i).range ≤ s
⊢ Membership.mem (α := N) s
    ((((lift (M := G) : (a : (i : ι) → G i →* N) → CoprodI G →* N) f : CoprodI G →* N) : (a : CoprodI G) → N) 1 : N)

Tactic:
exact s.one_mem

Premises used: Subgroup.one_mem
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : ι → Type u_4
inst : (i : ι) → Group (G i)
N : Type u_5
inst_1 : Group N
f : (i : ι) → MonoidHom.{u_4, u_5} (G i) N
s : Subgroup N
h : ∀ (i : ι), (f i).range ≤ s
i : ι
x : G i
of : Membership.mem (α := N) s ((f i : (a : G i) → N) x : N)
⊢ Membership.mem (α := N) s
    ((((lift (M := G) : (a : (i : ι) → G i →* N) → CoprodI G →* N) f : CoprodI G →* N) : (a : CoprodI G) → N)
        ((CoprodI.of (M := G) : (a : G i) → CoprodI G) x : CoprodI G) :
      N)

Tactic:
simp only [lift_of]

Premises used: Monoid.CoprodI.lift_of
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : ι → Type u_4
inst : (i : ι) → Group (G i)
N : Type u_5
inst_1 : Group N
f : (i : ι) → MonoidHom.{u_4, u_5} (G i) N
s : Subgroup N
h : ∀ (i : ι), (f i).range ≤ s
i : ι
x : G i
⊢ Membership.mem (α := N) s ((f i : (a : G i) → N) x : N)

Tactic:
h i (Set.mem_range_self x)

Premises used: Set.mem_range_self
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : ι → Type u_4
inst : (i : ι) → Group (G i)
N : Type u_5
inst_1 : Group N
f : (i : ι) → MonoidHom.{u_4, u_5} (G i) N
s : Subgroup N
h : ∀ (i : ι), (f i).range ≤ s
i : ι
x : G i
⊢ Membership.mem (α := N) s ((f i : (a : G i) → N) x : N)

Tactic:
exact h i (Set.mem_range_self x)

Premises used: Set.mem_range_self
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : ι → Type u_4
inst : (i : ι) → Group (G i)
N : Type u_5
inst_1 : Group N
f : (i : ι) → MonoidHom.{u_4, u_5} (G i) N
s : Subgroup N
h : ∀ (i : ι), (f i).range ≤ s
x y : CoprodI G
hx :
  Membership.mem (α := N) s
    ((((lift (M := G) : (a : (i : ι) → G i →* N) → CoprodI G →* N) f : CoprodI G →* N) : (a : CoprodI G) → N) x : N)
hy :
  Membership.mem (α := N) s
    ((((lift (M := G) : (a : (i : ι) → G i →* N) → CoprodI G →* N) f : CoprodI G →* N) : (a : CoprodI G) → N) y : N)
mul :
  HMul.hMul (α := N) (β := N)
      ((((lift (M := G) : (a : (i : ι) → G i →* N) → CoprodI G →* N) f : CoprodI G →* N) : (a : CoprodI G) → N) x : N)
      ((((lift (M := G) : (a : (i : ι) → G i →* N) → CoprodI G →* N) f : CoprodI G →* N) : (a : CoprodI G) → N) y : N) ∈
    s
⊢ Membership.mem (α := N) s
    ((((lift (M := G) : (a : (i : ι) → G i →* N) → CoprodI G →* N) f : CoprodI G →* N) : (a : CoprodI G) → N) (x * y) :
      N)

Tactic:
simp only [map_mul]

Premises used: map_mul
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : ι → Type u_4
inst : (i : ι) → Group (G i)
N : Type u_5
inst_1 : Group N
f : (i : ι) → MonoidHom.{u_4, u_5} (G i) N
s : Subgroup N
h : ∀ (i : ι), (f i).range ≤ s
x y : CoprodI G
hx :
  Membership.mem (α := N) s
    ((((lift (M := G) : (a : (i : ι) → G i →* N) → CoprodI G →* N) f : CoprodI G →* N) : (a : CoprodI G) → N) x : N)
hy :
  Membership.mem (α := N) s
    ((((lift (M := G) : (a : (i : ι) → G i →* N) → CoprodI G →* N) f : CoprodI G →* N) : (a : CoprodI G) → N) y : N)
⊢ HMul.hMul (α := N) (β := N)
      ((((lift (M := G) : (a : (i : ι) → G i →* N) → CoprodI G →* N) f : CoprodI G →* N) : (a : CoprodI G) → N) x : N)
      ((((lift (M := G) : (a : (i : ι) → G i →* N) → CoprodI G →* N) f : CoprodI G →* N) : (a : CoprodI G) → N) y : N) ∈
    s

Tactic:
s.mul_mem hx hy

Premises used: Subgroup.mul_mem
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : ι → Type u_4
inst : (i : ι) → Group (G i)
N : Type u_5
inst_1 : Group N
f : (i : ι) → MonoidHom.{u_4, u_5} (G i) N
s : Subgroup N
h : ∀ (i : ι), (f i).range ≤ s
x y : CoprodI G
hx :
  Membership.mem (α := N) s
    ((((lift (M := G) : (a : (i : ι) → G i →* N) → CoprodI G →* N) f : CoprodI G →* N) : (a : CoprodI G) → N) x : N)
hy :
  Membership.mem (α := N) s
    ((((lift (M := G) : (a : (i : ι) → G i →* N) → CoprodI G →* N) f : CoprodI G →* N) : (a : CoprodI G) → N) y : N)
⊢ HMul.hMul (α := N) (β := N)
      ((((lift (M := G) : (a : (i : ι) → G i →* N) → CoprodI G →* N) f : CoprodI G →* N) : (a : CoprodI G) → N) x : N)
      ((((lift (M := G) : (a : (i : ι) → G i →* N) → CoprodI G →* N) f : CoprodI G →* N) : (a : CoprodI G) → N) y : N) ∈
    s

Tactic:
exact s.mul_mem hx hy

Premises used: Subgroup.mul_mem
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : ι → Type u_4
inst : (i : ι) → Group (G i)
N : Type u_5
inst_1 : Group N
f : (i : ι) → MonoidHom.{u_4, u_5} (G i) N
s : Subgroup N
h : ∀ (i : ι), (f i).range ≤ s
x : CoprodI G
one :
  Membership.mem (α := N) s
    ((((lift (M := G) : (a : (i : ι) → G i →* N) → CoprodI G →* N) f : CoprodI G →* N) : (a : CoprodI G) → N) 1 : N)
of :
  ∀ (i : ι) (x : G i),
    Membership.mem (α := N) s
      ((((lift (M := G) : (a : (i : ι) → G i →* N) → CoprodI G →* N) f : CoprodI G →* N) : (a : CoprodI G) → N)
          ((CoprodI.of (M := G) : (a : G i) → CoprodI G) x : CoprodI G) :
        N)
mul :
  ∀ (x y : CoprodI G)
    (hx :
      Membership.mem (α := N) s
        ((((lift (M := G) : (a : (i : ι) → G i →* N) → CoprodI G →* N) f : CoprodI G →* N) : (a : CoprodI G) → N) x :
          N))
    (hy :
      Membership.mem (α := N) s
        ((((lift (M := G) : (a : (i : ι) → G i →* N) → CoprodI G →* N) f : CoprodI G →* N) : (a : CoprodI G) → N) y :
          N)),
    Membership.mem (α := N) s
      ((((lift (M := G) : (a : (i : ι) → G i →* N) → CoprodI G →* N) f : CoprodI G →* N) : (a : CoprodI G) → N)
          (x * y) :
        N)
⊢ Membership.mem (α := N) s
    ((((lift (M := G) : (a : (i : ι) → G i →* N) → CoprodI G →* N) f : CoprodI G →* N) : (a : CoprodI G) → N) x : N)

Tactic:
induction x using CoprodI.induction_on with
  | one => exact s.one_mem
  | of i x =>
    simp only [lift_of]
    exact h i (Set.mem_range_self x)
  | mul x y hx hy =>
    simp only [map_mul]
    exact s.mul_mem hx hy

Premises used: Monoid.CoprodI.of, Monoid.CoprodI.lift_of, Subgroup.one_mem, map_mul
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : ι → Type u_4
inst : (i : ι) → Group (G i)
N : Type u_5
inst_1 : Group N
f : (i : ι) → MonoidHom.{u_4, u_5} (G i) N
apply :
  LE.le.{u_5} (α := Subgroup N) (⨆ (i : ι), (f i).range)
    (MonoidHom.range (G := CoprodI G) ((lift (M := G) : (a : (i : ι) → G i →* N) → CoprodI G →* N) f))
⊢ Eq.{u_5 + 1} (α := Subgroup N)
    (MonoidHom.range (G := CoprodI G) ((lift (M := G) : (a : (i : ι) → G i →* N) → CoprodI G →* N) f))
    (⨆ (i : ι), (f i).range)

Tactic:
apply le_antisymm (lift_range_le _ f fun i => le_iSup (fun i => MonoidHom.range (f i)) i)

Premises used: MonoidHom.range, le_iSup, le_antisymm, Monoid.CoprodI.lift_range_le
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : ι → Type u_4
inst : (i : ι) → Group (G i)
N : Type u_5
inst_1 : Group N
f : (i : ι) → MonoidHom.{u_4, u_5} (G i) N
apply :
  ∀ (i : ι),
    (f i).range ≤ MonoidHom.range (G := CoprodI G) ((lift (M := G) : (a : (i : ι) → G i →* N) → CoprodI G →* N) f)
⊢ LE.le.{u_5} (α := Subgroup N) (⨆ (i : ι), (f i).range)
    (MonoidHom.range (G := CoprodI G) ((lift (M := G) : (a : (i : ι) → G i →* N) → CoprodI G →* N) f))

Tactic:
apply iSup_le _

Premises used: iSup_le
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : ι → Type u_4
inst : (i : ι) → Group (G i)
N : Type u_5
inst_1 : Group N
f : (i : ι) → MonoidHom.{u_4, u_5} (G i) N
i : ι
x : G i
⊢ Eq.{u_5 + 1} (α := N)
    ((((lift (M := G) : (a : (i : ι) → G i →* N) → CoprodI G →* N) f : CoprodI G →* N) : (a : CoprodI G) → N)
        ((of (M := G) : (a : G i) → CoprodI G) x : CoprodI G) :
      N)
    ((f i : (a : G i) → N) x : N)

Tactic:
simp only [lift_of]

Premises used: Monoid.CoprodI.lift_of
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : ι → Type u_4
inst : (i : ι) → Group (G i)
N : Type u_5
inst_1 : Group N
f : (i : ι) → MonoidHom.{u_4, u_5} (G i) N
i : ι
x : G i
⊢ Membership.mem.{u_5, u_5} (α := N) (γ := Subgroup N)
    (MonoidHom.range (G := CoprodI G) ((lift (M := G) : (a : (i : ι) → G i →* N) → CoprodI G →* N) f))
    ((f i : (a : G i) → N) x : N)

Tactic:
exact ⟨of x, by simp only [lift_of]⟩
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
⊢ ∀ (l : (i : ι) × M i), Membership.mem (γ := List ((i : ι) × M i)) [] l → l.snd (β := fun (i : ι) ↦ M i) ≠ 1

Tactic:
simp
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
⊢ Eq (α := CoprodI M) (prod (M := M) (empty (M := M))) 1

Tactic:
rfl

Premises used: Monoid.CoprodI.Word.prod, List.foldr, rfl, List.prod
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
w : Word M
i : ι
⊢ ¬w.fstIdx (M := M) ≠ some i ↔ ¬∀ l ∈ w.toList (M := M).head?, i ≠ l.fst (β := fun (i : ι) ↦ M i)

Tactic:
simp [fstIdx]

Premises used: Monoid.CoprodI.Word.fstIdx
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
i : ι
tauto : fstIdx (M := M) (empty (M := M)) = some i → False
⊢ fstIdx (M := M) (empty (M := M)) ≠ some i

Tactic:
tauto
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
i : ι
m : M i
w : Word M
hmw : w.fstIdx (M := M) ≠ some i
h1 : m ≠ 1
simp :
  ∀ (l : (i : ι) × M i),
    l = Sigma.mk (β := fun (i : ι) ↦ M i) i m ∨ l ∈ w.toList (M := M) → l.snd (β := fun (i : ι) ↦ M i) ≠ 1
⊢ ∀ l ∈ Sigma.mk (β := fun (i : ι) ↦ M i) i m :: w.toList (M := M), l.snd (β := fun (i : ι) ↦ M i) ≠ 1

Tactic:
simp only [List.mem_cons]

Premises used: List.mem_cons
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
i : ι
m : M i
w : Word M
hmw : w.fstIdx (M := M) ≠ some i
h1 : m ≠ 1
⊢ (Sigma.mk (β := fun (i : ι) ↦ M i) i m).snd (β := fun (i : ι) ↦ M i) ≠ 1

Tactic:
h1
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
i : ι
m : M i
w : Word M
hmw : w.fstIdx (M := M) ≠ some i
h1 : m ≠ 1
⊢ (Sigma.mk (β := fun (i : ι) ↦ M i) i m).snd (β := fun (i : ι) ↦ M i) ≠ 1

Tactic:
exact h1
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
i : ι
m : M i
w : Word M
hmw : w.fstIdx (M := M) ≠ some i
h1 : m ≠ 1
l : (i : ι) × M i
hl : l ∈ w.toList (M := M)
⊢ l.snd (β := fun (i : ι) ↦ M i) ≠ 1

Tactic:
w.ne_one l hl

Premises used: Monoid.CoprodI.Word.ne_one
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
i : ι
m : M i
w : Word M
hmw : w.fstIdx (M := M) ≠ some i
h1 : m ≠ 1
l : (i : ι) × M i
hl : l ∈ w.toList (M := M)
⊢ l.snd (β := fun (i : ι) ↦ M i) ≠ 1

Tactic:
exact w.ne_one l hl

Premises used: Monoid.CoprodI.Word.ne_one
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
i : ι
m : M i
w : Word M
hmw : w.fstIdx (M := M) ≠ some i
h1 : m ≠ 1
⊢ (cons (M := M) m w hmw h1).fstIdx (M := M) = some i

Tactic:
simp [cons, fstIdx]

Premises used: Monoid.CoprodI.Word.fstIdx, Monoid.CoprodI.Word.cons
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
i : ι
m : M i
w : Word M
h1 : m ≠ 1
h2 : w.fstIdx (M := M) ≠ some i
⊢ (cons (M := M) m w h2 h1).prod (M := M) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) (w.prod (M := M))

Tactic:
simp [cons, prod, List.map_cons, List.prod_cons]

Premises used: List.map_cons, Monoid.CoprodI.Word.prod, Monoid.CoprodI.Word.cons, List.prod_cons
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : (i : ι) → DecidableEq (M i)
i : ι
p : Pair M i
hm : p.head (M := M) = 1
rw :
  prod (M := M)
      (if h : p.head (M := M) = 1 then p.tail (M := M) else cons (M := M) (p.head (M := M)) (p.tail (M := M)) ⋯ h) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
      (p.tail (M := M).prod (M := M))
rw₁ :
  p.tail (M := M).prod (M := M) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
      (p.tail (M := M).prod (M := M))
rw₂ : p.tail (M := M).prod (M := M) = (of (M := M) : (a : M i) → CoprodI M) 1 * p.tail (M := M).prod (M := M)
rw₃ : p.tail (M := M).prod (M := M) = 1 * p.tail (M := M).prod (M := M)
rw₄ rw₅ : p.tail (M := M).prod (M := M) = p.tail (M := M).prod (M := M)
⊢ (rcons (M := M) p).prod (M := M) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
      (p.tail (M := M).prod (M := M))

Tactic:
rw [rcons, dif_pos hm, hm, map_one, one_mul]

Premises used: dif_pos, map_one, Monoid.CoprodI.Word.rcons, one_mul
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
h : w.fstIdx (M := M) ≠ some i
m' : M i
w' : Word M
h' : w'.fstIdx (M := M) ≠ some i
he : rcons (M := M) (Pair.mk (M := M) m w h) = rcons (M := M) (Pair.mk (M := M) m' w' h')
pos : ∀ (hm : m = 1), Pair.mk (M := M) m w h = Pair.mk (M := M) m' w' h'
neg : ∀ (hm : ¬m = 1), Pair.mk (M := M) m w h = Pair.mk (M := M) m' w' h'
⊢ Pair.mk (M := M) m w h = Pair.mk (M := M) m' w' h'

Tactic:
by_cases hm : m = 1
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
h : w.fstIdx (M := M) ≠ some i
m' : M i
w' : Word M
h' : w'.fstIdx (M := M) ≠ some i
he : rcons (M := M) (Pair.mk (M := M) m w h) = rcons (M := M) (Pair.mk (M := M) m' w' h')
hm : m = 1
pos : ∀ (hm' : m' = 1), Pair.mk (M := M) m w h = Pair.mk (M := M) m' w' h'
neg : ∀ (hm' : ¬m' = 1), Pair.mk (M := M) m w h = Pair.mk (M := M) m' w' h'
⊢ Pair.mk (M := M) m w h = Pair.mk (M := M) m' w' h'

Tactic:
by_cases hm' : m' = 1
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
h : w.fstIdx (M := M) ≠ some i
m' : M i
w' : Word M
h' : w'.fstIdx (M := M) ≠ some i
he : rcons (M := M) (Pair.mk (M := M) m w h) = rcons (M := M) (Pair.mk (M := M) m' w' h')
hm : ¬m = 1
pos : ∀ (hm' : m' = 1), Pair.mk (M := M) m w h = Pair.mk (M := M) m' w' h'
neg : ∀ (hm' : ¬m' = 1), Pair.mk (M := M) m w h = Pair.mk (M := M) m' w' h'
⊢ Pair.mk (M := M) m w h = Pair.mk (M := M) m' w' h'

Tactic:
by_cases hm' : m' = 1
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
h : w.fstIdx (M := M) ≠ some i
m' : M i
w' : Word M
h' : w'.fstIdx (M := M) ≠ some i
he : rcons (M := M) (Pair.mk (M := M) m w h) = rcons (M := M) (Pair.mk (M := M) m' w' h')
hm : m = 1
hm' : m' = 1
⊢ w = w'

Tactic:
simp only [rcons, dif_pos hm, dif_pos hm'] at he

Premises used: dif_pos, Monoid.CoprodI.Word.rcons
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
h : w.fstIdx (M := M) ≠ some i
m' : M i
w' : Word M
h' : w'.fstIdx (M := M) ≠ some i
hm : m = 1
hm' : m' = 1
he : w = w'
⊢ Pair.mk (M := M) m w h = Pair.mk (M := M) m' w' h'

Tactic:
simp_all
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
h : w.fstIdx (M := M) ≠ some i
m' : M i
w' : Word M
h' : w'.fstIdx (M := M) ≠ some i
he : rcons (M := M) (Pair.mk (M := M) m w h) = rcons (M := M) (Pair.mk (M := M) m' w' h')
hm : m = 1
hm' : ¬m' = 1
neg : False
⊢ Pair.mk (M := M) m w h = Pair.mk (M := M) m' w' h'

Tactic:
exfalso
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
h : w.fstIdx (M := M) ≠ some i
m' : M i
w' : Word M
h' : w'.fstIdx (M := M) ≠ some i
he : rcons (M := M) (Pair.mk (M := M) m w h) = rcons (M := M) (Pair.mk (M := M) m' w' h')
hm : m = 1
hm' : ¬m' = 1
⊢ w = cons (M := M) m' w' ⋯ ⋯

Tactic:
simp only [rcons, dif_pos hm, dif_neg hm'] at he

Premises used: dif_pos, dif_neg, Monoid.CoprodI.Word.rcons
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
h : w.fstIdx (M := M) ≠ some i
m' : M i
w' : Word M
h' : w'.fstIdx (M := M) ≠ some i
hm : m = 1
hm' : ¬m' = 1
he : w = cons (M := M) m' w' ⋯ ⋯
⊢ (cons (M := M) m' w' ⋯ ⋯).fstIdx (M := M) ≠ some i

Tactic:
rw [he] at h
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
h : w.fstIdx (M := M) ≠ some i
m' : M i
w' : Word M
h' : w'.fstIdx (M := M) ≠ some i
hm : m = 1
hm' : ¬m' = 1
he : w = cons (M := M) m' w' ⋯ ⋯
h₁ : (cons (M := M) m' w' ⋯ ⋯).fstIdx (M := M) ≠ some i
⊢ w = cons (M := M) m' w' ⋯ ⋯

Tactic:
rw [he] at h
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
m' : M i
w' : Word M
h' : w'.fstIdx (M := M) ≠ some i
hm : m = 1
hm' : ¬m' = 1
h : (cons (M := M) m' w' ⋯ ⋯).fstIdx (M := M) ≠ some i
he : w = cons (M := M) m' w' ⋯ ⋯
⊢ False

Tactic:
h rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
m' : M i
w' : Word M
h' : w'.fstIdx (M := M) ≠ some i
hm : m = 1
hm' : ¬m' = 1
h : (cons (M := M) m' w' ⋯ ⋯).fstIdx (M := M) ≠ some i
he : w = cons (M := M) m' w' ⋯ ⋯
⊢ False

Tactic:
exact h rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
h : w.fstIdx (M := M) ≠ some i
m' : M i
w' : Word M
h' : w'.fstIdx (M := M) ≠ some i
he : rcons (M := M) (Pair.mk (M := M) m w h) = rcons (M := M) (Pair.mk (M := M) m' w' h')
hm : ¬m = 1
hm' : m' = 1
pos : False
⊢ Pair.mk (M := M) m w h = Pair.mk (M := M) m' w' h'

Tactic:
exfalso
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
h : w.fstIdx (M := M) ≠ some i
m' : M i
w' : Word M
h' : w'.fstIdx (M := M) ≠ some i
he : rcons (M := M) (Pair.mk (M := M) m w h) = rcons (M := M) (Pair.mk (M := M) m' w' h')
hm : ¬m = 1
hm' : m' = 1
⊢ cons (M := M) m w ⋯ ⋯ = w'

Tactic:
simp only [rcons, dif_pos hm', dif_neg hm] at he

Premises used: dif_pos, dif_neg, Monoid.CoprodI.Word.rcons
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
h : w.fstIdx (M := M) ≠ some i
m' : M i
w' : Word M
h' : w'.fstIdx (M := M) ≠ some i
hm : ¬m = 1
hm' : m' = 1
he : cons (M := M) m w ⋯ ⋯ = w'
⊢ (cons (M := M) m w ⋯ ⋯).fstIdx (M := M) ≠ some i

Tactic:
rw [← he] at h'
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
h : w.fstIdx (M := M) ≠ some i
m' : M i
w' : Word M
h' : w'.fstIdx (M := M) ≠ some i
hm : ¬m = 1
hm' : m' = 1
he : cons (M := M) m w ⋯ ⋯ = w'
h'₁ : (cons (M := M) m w ⋯ ⋯).fstIdx (M := M) ≠ some i
⊢ m' = 1

Tactic:
rw [← he] at h'
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
h : w.fstIdx (M := M) ≠ some i
m' : M i
w' : Word M
h' : w'.fstIdx (M := M) ≠ some i
hm : ¬m = 1
hm' : m' = 1
he : cons (M := M) m w ⋯ ⋯ = w'
h'₁ : (cons (M := M) m w ⋯ ⋯).fstIdx (M := M) ≠ some i
hm'₁ : m' = 1
⊢ cons (M := M) m w ⋯ ⋯ = w'

Tactic:
rw [← he] at h'
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
h : w.fstIdx (M := M) ≠ some i
m' : M i
w' : Word M
hm : ¬m = 1
h' : (cons (M := M) m w ⋯ ⋯).fstIdx (M := M) ≠ some i
hm' : m' = 1
he : cons (M := M) m w ⋯ ⋯ = w'
⊢ False

Tactic:
h' rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
h : w.fstIdx (M := M) ≠ some i
m' : M i
w' : Word M
hm : ¬m = 1
h' : (cons (M := M) m w ⋯ ⋯).fstIdx (M := M) ≠ some i
hm' : m' = 1
he : cons (M := M) m w ⋯ ⋯ = w'
⊢ False

Tactic:
exact h' rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
h : w.fstIdx (M := M) ≠ some i
m' : M i
w' : Word M
h' : w'.fstIdx (M := M) ≠ some i
he : rcons (M := M) (Pair.mk (M := M) m w h) = rcons (M := M) (Pair.mk (M := M) m' w' h')
hm : ¬m = 1
hm' : ¬m' = 1
⊢ m = m' ∧ w.toList (M := M) = w'.toList (M := M)

Tactic:
simpa [cons, rcons, dif_neg hm, dif_neg hm', eq_self_iff_true, Subtype.mk_eq_mk,
        heq_iff_eq, ← Subtype.ext_iff] using he

Premises used: heq_iff_eq, dif_neg, Subtype.ext_iff, Monoid.CoprodI.Word.rcons, Subtype.mk_eq_mk, Monoid.CoprodI.Word.cons, eq_self_iff_true
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
h : w.fstIdx (M := M) ≠ some i
m' : M i
w' : Word M
h' : w'.fstIdx (M := M) ≠ some i
he : rcons (M := M) (Pair.mk (M := M) m w h) = rcons (M := M) (Pair.mk (M := M) m' w' h')
hm : ¬m = 1
hm' : ¬m' = 1
⊢ m = m' ∧ w.toList (M := M) = w'.toList (M := M)

Tactic:
have : m = m' ∧ w.toList = w'.toList := by
      simpa [cons, rcons, dif_neg hm, dif_neg hm', eq_self_iff_true, Subtype.mk_eq_mk,
        heq_iff_eq, ← Subtype.ext_iff] using he