awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι : Type u_1
M : Type u_2
S : Type u_4
inst : Monoid M
inst_1 : LinearOrder S
inst_2 : CommMonoid S
inst_3 : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
i : ι
hv_one : v i ≠ 1
hi :
  Membership.mem (γ := Submonoid M)
    (closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)})) (v i)
x y : M
h :
  Membership.mem (γ := Submonoid M)
    (closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)})) x
h_1 :
  Membership.mem (γ := Submonoid M)
    (closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)})) y
hx : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) x : S)
hy : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) y : S)
⊢ LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (x * y) : S)

Tactic:
simpa only [map_mul] using Left.one_lt_mul hx hy

Premises used: Left.one_lt_mul, map_mul
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι : Type u_1
G : Type u_3
S : Type u_4
inst : CommGroup G
inst_1 : LinearOrder S
inst_2 : InvolutiveInv ι
inst_3 : CommGroup S
inst_4 : IsOrderedMonoid S
v : ι → G
f : G →* S
s : Set ι
hf : ∀ i ∈ s, LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
hsp :
  Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i) ∨
    Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)⁻¹
inr :
  ∀
    (this :
      ∀ {ι : Type u_1} {G : Type u_3} {S : Type u_4} [inst : CommGroup G] [inst_5 : LinearOrder S]
        [inst_6 : InvolutiveInv ι] [inst_7 : CommGroup S] [IsOrderedMonoid S] (v : ι → G) (f : G →* S) (s : Set ι)
        (hf : ∀ i ∈ s, LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)) (i : ι) (hv_one : v i ≠ 1)
        (hv_inv : v i⁻¹ = (v i)⁻¹)
        (hsp :
          Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i) ∨
            Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)⁻¹)
        (hi : Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)),
        Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S))
    (hi : v i ∉ closure (v '' s)), Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
wlog :
  ∀ {ι : Type u_1} {G : Type u_3} {S : Type u_4} [inst : CommGroup G] [inst_5 : LinearOrder S]
    [inst_6 : InvolutiveInv ι] [inst_7 : CommGroup S] [IsOrderedMonoid S] (v : ι → G) (f : G →* S) (s : Set ι)
    (hf : ∀ i ∈ s, LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)) (i : ι) (hv_one : v i ≠ 1)
    (hv_inv : v i⁻¹ = (v i)⁻¹)
    (hsp :
      Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i) ∨
        Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)⁻¹)
    (hi : Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)),
    Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
⊢ Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)

Tactic:
wlog hi : v i ∈ closure (v '' s)

Premises used: Submonoid.closure, Set.image
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι : Type u_1
G : Type u_3
S : Type u_4
inst : CommGroup G
inst_1 : LinearOrder S
inst_2 : InvolutiveInv ι
inst_3 : CommGroup S
inst_4 : IsOrderedMonoid S
v : ι → G
f : G →* S
s : Set ι
hf : ∀ i ∈ s, LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
hsp :
  Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i) ∨
    Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)⁻¹
this :
  ∀ {ι : Type u_1} {G : Type u_3} {S : Type u_4} [inst : CommGroup G] [inst_5 : LinearOrder S]
    [inst_6 : InvolutiveInv ι] [inst_7 : CommGroup S] [IsOrderedMonoid S] (v : ι → G) (f : G →* S) (s : Set ι)
    (hf : ∀ i ∈ s, LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)) (i : ι) (hv_one : v i ≠ 1)
    (hv_inv : v i⁻¹ = (v i)⁻¹)
    (hsp :
      Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i) ∨
        Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)⁻¹)
    (hi : Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)),
    Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
hi : v i ∉ closure (v '' s)
inr :
  ∀ (hi' : Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)),
    Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
inr₁ :
  ∀ (hi' : Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)⁻¹),
    Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
⊢ Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)

Tactic:
rcases hsp with hi' | hi'
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι : Type u_1
G : Type u_3
S : Type u_4
inst : CommGroup G
inst_1 : LinearOrder S
inst_2 : InvolutiveInv ι
inst_3 : CommGroup S
inst_4 : IsOrderedMonoid S
v : ι → G
f : G →* S
s : Set ι
hf : ∀ i ∈ s, LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
this :
  ∀ {ι : Type u_1} {G : Type u_3} {S : Type u_4} [inst : CommGroup G] [inst_5 : LinearOrder S]
    [inst_6 : InvolutiveInv ι] [inst_7 : CommGroup S] [IsOrderedMonoid S] (v : ι → G) (f : G →* S) (s : Set ι)
    (hf : ∀ i ∈ s, LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)) (i : ι) (hv_one : v i ≠ 1)
    (hv_inv : v i⁻¹ = (v i)⁻¹)
    (hsp :
      Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i) ∨
        Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)⁻¹)
    (hi : Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)),
    Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
hi : v i ∉ closure (v '' s)
hi' : Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)
⊢ Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)

Tactic:
contradiction
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι : Type u_1
G : Type u_3
S : Type u_4
inst : CommGroup G
inst_1 : LinearOrder S
inst_2 : InvolutiveInv ι
inst_3 : CommGroup S
inst_4 : IsOrderedMonoid S
v : ι → G
f : G →* S
s : Set ι
hf : ∀ i ∈ s, LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
this :
  ∀ {ι : Type u_1} {G : Type u_3} {S : Type u_4} [inst : CommGroup G] [inst_5 : LinearOrder S]
    [inst_6 : InvolutiveInv ι] [inst_7 : CommGroup S] [IsOrderedMonoid S] (v : ι → G) (f : G →* S) (s : Set ι)
    (hf : ∀ i ∈ s, LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)) (i : ι) (hv_one : v i ≠ 1)
    (hv_inv : v i⁻¹ = (v i)⁻¹)
    (hsp :
      Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i) ∨
        Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)⁻¹)
    (hi : Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)),
    Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
hi : v i ∉ closure (v '' s)
hi' : Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)⁻¹
⊢ v i⁻¹ ≠ 1

Tactic:
simpa [hv_inv]
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι : Type u_1
G : Type u_3
S : Type u_4
inst : CommGroup G
inst_1 : LinearOrder S
inst_2 : InvolutiveInv ι
inst_3 : CommGroup S
inst_4 : IsOrderedMonoid S
v : ι → G
f : G →* S
s : Set ι
hf : ∀ i ∈ s, LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
this :
  ∀ {ι : Type u_1} {G : Type u_3} {S : Type u_4} [inst : CommGroup G] [inst_5 : LinearOrder S]
    [inst_6 : InvolutiveInv ι] [inst_7 : CommGroup S] [IsOrderedMonoid S] (v : ι → G) (f : G →* S) (s : Set ι)
    (hf : ∀ i ∈ s, LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)) (i : ι) (hv_one : v i ≠ 1)
    (hv_inv : v i⁻¹ = (v i)⁻¹)
    (hsp :
      Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i) ∨
        Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)⁻¹)
    (hi : Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)),
    Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
hi : v i ∉ closure (v '' s)
hi' : Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)⁻¹
⊢ v i⁻¹⁻¹ = (v i⁻¹)⁻¹

Tactic:
simp [hv_inv]
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι : Type u_1
G : Type u_3
S : Type u_4
inst : CommGroup G
inst_1 : LinearOrder S
inst_2 : InvolutiveInv ι
inst_3 : CommGroup S
inst_4 : IsOrderedMonoid S
v : ι → G
f : G →* S
s : Set ι
hf : ∀ i ∈ s, LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
this :
  ∀ {ι : Type u_1} {G : Type u_3} {S : Type u_4} [inst : CommGroup G] [inst_5 : LinearOrder S]
    [inst_6 : InvolutiveInv ι] [inst_7 : CommGroup S] [IsOrderedMonoid S] (v : ι → G) (f : G →* S) (s : Set ι)
    (hf : ∀ i ∈ s, LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)) (i : ι) (hv_one : v i ≠ 1)
    (hv_inv : v i⁻¹ = (v i)⁻¹)
    (hsp :
      Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i) ∨
        Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)⁻¹)
    (hi : Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)),
    Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
hi : v i ∉ closure (v '' s)
hi' : Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)⁻¹
h : Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i⁻¹)
⊢ Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i⁻¹) ∨
    Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i⁻¹)⁻¹

Tactic:
left
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι : Type u_1
G : Type u_3
S : Type u_4
inst : CommGroup G
inst_1 : LinearOrder S
inst_2 : InvolutiveInv ι
inst_3 : CommGroup S
inst_4 : IsOrderedMonoid S
v : ι → G
f : G →* S
s : Set ι
hf : ∀ i ∈ s, LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
this :
  ∀ {ι : Type u_1} {G : Type u_3} {S : Type u_4} [inst : CommGroup G] [inst_5 : LinearOrder S]
    [inst_6 : InvolutiveInv ι] [inst_7 : CommGroup S] [IsOrderedMonoid S] (v : ι → G) (f : G →* S) (s : Set ι)
    (hf : ∀ i ∈ s, LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)) (i : ι) (hv_one : v i ≠ 1)
    (hv_inv : v i⁻¹ = (v i)⁻¹)
    (hsp :
      Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i) ∨
        Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)⁻¹)
    (hi : Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)),
    Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
hi : v i ∉ closure (v '' s)
hi' : Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)⁻¹
⊢ Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i⁻¹)

Tactic:
simpa [hv_inv]
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι : Type u_1
G : Type u_3
S : Type u_4
inst : CommGroup G
inst_1 : LinearOrder S
inst_2 : InvolutiveInv ι
inst_3 : CommGroup S
inst_4 : IsOrderedMonoid S
v : ι → G
f : G →* S
s : Set ι
hf : ∀ i ∈ s, LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
this :
  ∀ {ι : Type u_1} {G : Type u_3} {S : Type u_4} [inst : CommGroup G] [inst_5 : LinearOrder S]
    [inst_6 : InvolutiveInv ι] [inst_7 : CommGroup S] [IsOrderedMonoid S] (v : ι → G) (f : G →* S) (s : Set ι)
    (hf : ∀ i ∈ s, LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)) (i : ι) (hv_one : v i ≠ 1)
    (hv_inv : v i⁻¹ = (v i)⁻¹)
    (hsp :
      Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i) ∨
        Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)⁻¹)
    (hi : Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)),
    Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)
hi : v i ∉ closure (v '' s)
hi' : Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)⁻¹
⊢ Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)

Tactic:
simpa [hv_inv] using this v f s hf i⁻¹ (by simpa [hv_inv]) (by simp [hv_inv])
      (by left; simpa [hv_inv]) (by simpa [hv_inv])

Premises used: Inv.inv
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι_1 : Type u_1
G_1 : Type u_3
S_1 : Type u_4
inst : CommGroup G_1
inst_1 : LinearOrder S_1
ι : Type u_1
G : Type u_3
S : Type u_4
inst_2 : CommGroup G
inst_3 : LinearOrder S
inst_4 : InvolutiveInv ι
inst_5 : CommGroup S
inst_6 : IsOrderedMonoid S
v : ι → G
f : G →* S
s : Set ι
hf : ∀ i ∈ s, LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
hsp :
  Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i) ∨
    Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)⁻¹
hi : Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)
suffices : v i ≠ 1 → LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)
⊢ Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S)

Tactic:
suffices v i ≠ 1 → 1 < f (v i) from (this hv_one).ne'
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι_1 : Type u_1
G_1 : Type u_3
S_1 : Type u_4
inst : CommGroup G_1
inst_1 : LinearOrder S_1
ι : Type u_1
G : Type u_3
S : Type u_4
inst_2 : CommGroup G
inst_3 : LinearOrder S
inst_4 : InvolutiveInv ι
inst_5 : CommGroup S
inst_6 : IsOrderedMonoid S
v : ι → G
f : G →* S
s : Set ι
hf : ∀ i ∈ s, LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
hsp :
  Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i) ∨
    Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)⁻¹
hi : Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)
⊢ ∀ (x : G) (h : x ∈ v '' s), x ≠ 1 → LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) x : S)

Tactic:
simp_all
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι_1 : Type u_1
G_1 : Type u_3
S_1 : Type u_4
inst : CommGroup G_1
inst_1 : LinearOrder S_1
ι : Type u_1
G : Type u_3
S : Type u_4
inst_2 : CommGroup G
inst_3 : LinearOrder S
inst_4 : InvolutiveInv ι
inst_5 : CommGroup S
inst_6 : IsOrderedMonoid S
v : ι → G
f : G →* S
s : Set ι
hf : ∀ i ∈ s, LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
hsp :
  Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i) ∨
    Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)⁻¹
hi : Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)
⊢ Ne.{u_3 + 1} (α := G) 1 1 → LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) 1 : S)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι_1 : Type u_1
G_1 : Type u_3
S_1 : Type u_4
inst : CommGroup G_1
inst_1 : LinearOrder S_1
ι : Type u_1
G : Type u_3
S : Type u_4
inst_2 : CommGroup G
inst_3 : LinearOrder S
inst_4 : InvolutiveInv ι
inst_5 : CommGroup S
inst_6 : IsOrderedMonoid S
v : ι → G
f : G →* S
s : Set ι
hf : ∀ i ∈ s, LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
hsp :
  Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i) ∨
    Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)⁻¹
hi : Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)
refine :
  ∀ (x y : G),
    Membership.mem (γ := Submonoid G) (closure (v '' s)) x →
      Membership.mem (γ := Submonoid G) (closure (v '' s)) y →
        ∀ (hx : x ≠ 1 → LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) x : S))
          (hy : y ≠ 1 → LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) y : S)),
          x * y ≠ 1 → LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (x * y) : S)
⊢ v i ≠ 1 → LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)

Tactic:
refine closure_induction (by simp_all) (by simp) (fun x y _ _ hx hy _ ↦ ?_) hi
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι_1 : Type u_1
G_1 : Type u_3
S_1 : Type u_4
inst : CommGroup G_1
inst_1 : LinearOrder S_1
ι : Type u_1
G : Type u_3
S : Type u_4
inst_2 : CommGroup G
inst_3 : LinearOrder S
inst_4 : InvolutiveInv ι
inst_5 : CommGroup S
inst_6 : IsOrderedMonoid S
v : ι → G
f : G →* S
s : Set ι
hf : ∀ i ∈ s, LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
hsp :
  Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i) ∨
    Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)⁻¹
hi : Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)
x y : G
h : Membership.mem (γ := Submonoid G) (closure (v '' s)) x
h_1 : Membership.mem (γ := Submonoid G) (closure (v '' s)) y
hx : x ≠ 1 → LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) x : S)
hy : y ≠ 1 → LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) y : S)
h_2 : x * y ≠ 1
inl :
  Membership.mem (γ := Submonoid G) (closure (v '' s)) 1 →
    ∀ (hx : Ne.{u_3 + 1} (α := G) 1 1 → LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) 1 : S)),
      1 * y ≠ 1 → LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (1 * y) : S)
inr : ∀ (hx' : x ≠ 1), LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (x * y) : S)
⊢ LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (x * y) : S)

Tactic:
rcases eq_or_ne x 1 with rfl | hx'

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι_1 : Type u_1
G_1 : Type u_3
S_1 : Type u_4
inst : CommGroup G_1
inst_1 : LinearOrder S_1
ι : Type u_1
G : Type u_3
S : Type u_4
inst_2 : CommGroup G
inst_3 : LinearOrder S
inst_4 : InvolutiveInv ι
inst_5 : CommGroup S
inst_6 : IsOrderedMonoid S
v : ι → G
f : G →* S
s : Set ι
hf : ∀ i ∈ s, LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
hsp :
  Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i) ∨
    Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)⁻¹
hi : Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)
y : G
h : Membership.mem (γ := Submonoid G) (closure (v '' s)) y
hy : y ≠ 1 → LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) y : S)
h_1 : Membership.mem (γ := Submonoid G) (closure (v '' s)) 1
hx : Ne.{u_3 + 1} (α := G) 1 1 → LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) 1 : S)
h_2 : 1 * y ≠ 1
⊢ LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (1 * y) : S)

Tactic:
grind
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι_1 : Type u_1
G_1 : Type u_3
S_1 : Type u_4
inst : CommGroup G_1
inst_1 : LinearOrder S_1
ι : Type u_1
G : Type u_3
S : Type u_4
inst_2 : CommGroup G
inst_3 : LinearOrder S
inst_4 : InvolutiveInv ι
inst_5 : CommGroup S
inst_6 : IsOrderedMonoid S
v : ι → G
f : G →* S
s : Set ι
hf : ∀ i ∈ s, LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
hsp :
  Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i) ∨
    Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)⁻¹
hi : Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)
x y : G
h : Membership.mem (γ := Submonoid G) (closure (v '' s)) x
h_1 : Membership.mem (γ := Submonoid G) (closure (v '' s)) y
hx : x ≠ 1 → LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) x : S)
hy : y ≠ 1 → LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) y : S)
h_2 : x * y ≠ 1
hx' : x ≠ 1
inr :
  Membership.mem (γ := Submonoid G) (closure (v '' s)) 1 →
    ∀ (hy : Ne.{u_3 + 1} (α := G) 1 1 → LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) 1 : S)),
      x * 1 ≠ 1 → LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (x * 1) : S)
inr₁ : ∀ (hy' : y ≠ 1), LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (x * y) : S)
⊢ LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (x * y) : S)

Tactic:
rcases eq_or_ne y 1 with rfl | hy'

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι_1 : Type u_1
G_1 : Type u_3
S_1 : Type u_4
inst : CommGroup G_1
inst_1 : LinearOrder S_1
ι : Type u_1
G : Type u_3
S : Type u_4
inst_2 : CommGroup G
inst_3 : LinearOrder S
inst_4 : InvolutiveInv ι
inst_5 : CommGroup S
inst_6 : IsOrderedMonoid S
v : ι → G
f : G →* S
s : Set ι
hf : ∀ i ∈ s, LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
hsp :
  Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i) ∨
    Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)⁻¹
hi : Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)
x : G
h : Membership.mem (γ := Submonoid G) (closure (v '' s)) x
hx : x ≠ 1 → LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) x : S)
hx' : x ≠ 1
h_1 : Membership.mem (γ := Submonoid G) (closure (v '' s)) 1
hy : Ne.{u_3 + 1} (α := G) 1 1 → LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) 1 : S)
h_2 : x * 1 ≠ 1
⊢ LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (x * 1) : S)

Tactic:
grind
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι_1 : Type u_1
G_1 : Type u_3
S_1 : Type u_4
inst : CommGroup G_1
inst_1 : LinearOrder S_1
ι : Type u_1
G : Type u_3
S : Type u_4
inst_2 : CommGroup G
inst_3 : LinearOrder S
inst_4 : InvolutiveInv ι
inst_5 : CommGroup S
inst_6 : IsOrderedMonoid S
v : ι → G
f : G →* S
s : Set ι
hf : ∀ i ∈ s, LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
hsp :
  Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i) ∨
    Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)⁻¹
hi : Membership.mem (γ := Submonoid G) (closure (v '' s)) (v i)
x y : G
h : Membership.mem (γ := Submonoid G) (closure (v '' s)) x
h_1 : Membership.mem (γ := Submonoid G) (closure (v '' s)) y
hx : x ≠ 1 → LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) x : S)
hy : y ≠ 1 → LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) y : S)
h_2 : x * y ≠ 1
hx' : x ≠ 1
hy' : y ≠ 1
⊢ LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (x * y) : S)

Tactic:
simpa using lt_mul_of_lt_of_one_lt (hx hx') (hy hy')

Premises used: lt_mul_of_lt_of_one_lt
-- Module: Mathlib.Algebra.Group.Irreducible.Indecomposable
Goal:
ι : Type u_1
G : Type u_3
S : Type u_4
inst : CommGroup G
inst_1 : LinearOrder S
inst_2 : Finite ι
inst_3 : InvolutiveInv ι
inst_4 : CommGroup S
inst_5 : IsOrderedMonoid S
v : ι → G
f : G →* S
i : ι
hi : v i ≠ 1
hi' : v i⁻¹ = (v i)⁻¹
⊢ Ne.{u_4 + 1} (α := S) ((f : (a : G) → S) (v i) : S) (1 : S) ↔
    Membership.mem (γ := Submonoid G) (closure (v '' baseOf v f)) (v i) ∨
      Membership.mem (γ := Submonoid G) (closure (v '' baseOf v f)) (v i)⁻¹

Tactic:
⟨fun h ↦ mem_or_inv_mem_closure_baseOf v f i h hi',
    apply_ne_one_of_mem_or_inv_mem_closure v f (baseOf v f) (baseOf_subset_one_lt v f) i hi hi'⟩

Premises used: Submonoid.apply_ne_one_of_mem_or_inv_mem_closure, IsMulIndecomposable.mem_or_inv_mem_closure_baseOf, IsMulIndecomposable.baseOf_subset_one_lt, IsMulIndecomposable.baseOf, Iff.intro
-- Module: Mathlib.Algebra.Group.Irreducible.Lemmas
Goal:
M : Type u_2
inst : Monoid M
x : M
h : Ne (α := ℕ) 0 1
⊢ ¬Irreducible (HPow.hPow (β := ℕ) x 0)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Irreducible.Lemmas
Goal:
M : Type u_2
inst : Monoid M
x : M
n : ℕ
h : n + 2 ≠ 1
h₁ : ¬IsUnit (x ^ (n + 2))
h₂ : ∀ ⦃a b : M⦄, x ^ (n + 2) = a * b → IsUnit a ∨ IsUnit b
⊢ IsUnit (x ^ (n + 1)) ∨ IsUnit x

Tactic:
have := h₂ (pow_succ _ _)
-- Module: Mathlib.Algebra.Group.Irreducible.Lemmas
Goal:
M : Type u_2
inst : Monoid M
x : M
n : ℕ
h : n + 2 ≠ 1
h₁ : ¬IsUnit (x ^ (n + 2))
h₂ : ∀ ⦃a b : M⦄, x ^ (n + 2) = a * b → IsUnit a ∨ IsUnit b
this : IsUnit (x ^ (n + 1)) ∨ IsUnit x
⊢ IsUnit x

Tactic:
rw [isUnit_pow_iff n.succ_ne_zero, or_self] at this

Premises used: isUnit_pow_iff, Nat.succ_ne_zero, or_self
-- Module: Mathlib.Algebra.Group.Irreducible.Lemmas
Goal:
M : Type u_2
inst : Monoid M
x : M
n : ℕ
h : n + 2 ≠ 1
h₁ : ¬IsUnit (x ^ (n + 2))
h₂ : ∀ ⦃a b : M⦄, x ^ (n + 2) = a * b → IsUnit a ∨ IsUnit b
this : IsUnit x
⊢ False

Tactic:
h₁ (this.pow _)

Premises used: IsUnit.pow
-- Module: Mathlib.Algebra.Group.Irreducible.Lemmas
Goal:
M : Type u_2
inst : Monoid M
x : M
n : ℕ
h : n + 2 ≠ 1
h₁ : ¬IsUnit (x ^ (n + 2))
h₂ : ∀ ⦃a b : M⦄, x ^ (n + 2) = a * b → IsUnit a ∨ IsUnit b
this : IsUnit x
⊢ False

Tactic:
exact h₁ (this.pow _)

Premises used: IsUnit.pow
-- Module: Mathlib.Algebra.Group.Irreducible.Lemmas
Goal:
M : Type u_2
inst : Monoid M
y : M
u : Mˣ
simp :
  ¬IsUnit y → ((∀ ⦃a b : M⦄, (↑u : M) * y = a * b → IsUnit a ∨ IsUnit b) ↔ ∀ ⦃a b : M⦄, y = a * b → IsUnit a ∨ IsUnit b)
⊢ Irreducible ((↑u : M) * y) ↔ Irreducible y

Tactic:
simp only [irreducible_iff, Units.isUnit_units_mul, and_congr_right_iff]

Premises used: and_congr_right_iff, Units.isUnit_units_mul, irreducible_iff