awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
i : ι
hi_1 :
  Membership.mem (γ := Set ι)
    {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((MonoidHom.comp invMonoidHom f : (a : G) → S) (v i) : S)} i
hi' :
  ∀ (j : ι),
    Membership.mem (γ := Set ι)
        {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((MonoidHom.comp invMonoidHom f : (a : G) → S) (v i) : S)} j →
      ∀ (k : ι),
        Membership.mem (γ := Set ι)
            {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((MonoidHom.comp invMonoidHom f : (a : G) → S) (v i) : S)} k →
          v i = v j * v k → v j = 1 ∨ v k = 1
j : ι
hj : Membership.mem (γ := Set ι) {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} j
k : ι
hk : Membership.mem (γ := Set ι) {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} k
hi : v i = v j⁻¹ * v k⁻¹
⊢ Membership.mem (γ := Set ι)
    {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((MonoidHom.comp invMonoidHom f : (a : G) → S) (v i) : S)} k⁻¹

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
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
i : ι
hi_1 :
  Membership.mem (γ := Set ι)
    {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((MonoidHom.comp invMonoidHom f : (a : G) → S) (v i) : S)} i
hi' :
  ∀ (j : ι),
    Membership.mem (γ := Set ι)
        {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((MonoidHom.comp invMonoidHom f : (a : G) → S) (v i) : S)} j →
      ∀ (k : ι),
        Membership.mem (γ := Set ι)
            {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((MonoidHom.comp invMonoidHom f : (a : G) → S) (v i) : S)} k →
          v i = v j * v k → v j = 1 ∨ v k = 1
j : ι
hj : Membership.mem (γ := Set ι) {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} j
k : ι
hk : Membership.mem (γ := Set ι) {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} k
hi : v i = v j⁻¹ * v k⁻¹
⊢ v j⁻¹ = 1 ∨ v k⁻¹ = 1

Tactic:
specialize hi' j⁻¹ (by simpa [hv_inv]) k⁻¹ (by simpa [hv_inv]) hi

Premises used: Inv.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
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
i : ι
hi_1 :
  Membership.mem (γ := Set ι)
    {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((MonoidHom.comp invMonoidHom f : (a : G) → S) (v i) : S)} i
j : ι
hj : Membership.mem (γ := Set ι) {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} j
k : ι
hk : Membership.mem (γ := Set ι) {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : G) → S) (v i) : S)} k
hi : v i = v j⁻¹ * v k⁻¹
hi' : v j⁻¹ = 1 ∨ v k⁻¹ = 1
⊢ v j = 1 ∨ v k = 1

Tactic:
aesop
-- 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 : Finite ι
inst_3 : CommMonoid S
inst_4 : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
⊢ Eq (α := Submonoid M) (closure (v '' IsMulIndecomposable.baseOf v f))
    (closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)}))

Tactic:
le_antisymm (closure_mono (image_mono <| IsMulIndecomposable.baseOf_subset_one_lt v f))
    (closure_le.mpr ?_)

Premises used: Iff.mpr, Set.image_mono, Submonoid.closure_mono, IsMulIndecomposable.baseOf_subset_one_lt, le_antisymm, Submonoid.closure_le
-- 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 : Finite ι
inst_3 : CommMonoid S
inst_4 : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
refine :
  v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)} ⊆
    (↑(closure (v '' IsMulIndecomposable.baseOf v f)) : Set M)
⊢ Eq (α := Submonoid M) (closure (v '' IsMulIndecomposable.baseOf v f))
    (closure (v '' {i : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)}))

Tactic:
refine le_antisymm (closure_mono (image_mono <| IsMulIndecomposable.baseOf_subset_one_lt v f))
    (closure_le.mpr ?_)

Premises used: Iff.mpr, Set.image_mono, Submonoid.closure_mono, IsMulIndecomposable.baseOf_subset_one_lt, le_antisymm, Submonoid.closure_le
-- 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 : Finite ι
inst_3 : CommMonoid S
inst_4 : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
i : ι
hi : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)
by_contra : ∀ (hi' : v i ∉ (↑(closure (v '' IsMulIndecomposable.baseOf v f)) : Set M)), False
⊢ v i ∈ (↑(closure (v '' IsMulIndecomposable.baseOf v f)) : Set M)

Tactic:
by_contra hi'
-- 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 : Finite ι
inst_3 : CommMonoid S
inst_4 : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
i : ι
hi : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)
hi' : v i ∉ (↑(closure (v '' IsMulIndecomposable.baseOf v f)) : Set M)
t : Set ι := {i : ι | IsMulIndecomposable v {j : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v j) : S)} i}
s : Set ι := {j : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v j) : S) ∧ v j ∉ closure (v '' t)}
⊢ s.Nonempty

Tactic:
have hne : s.Nonempty := ⟨i, hi, hi'⟩
-- 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 : Finite ι
inst_3 : CommMonoid S
inst_4 : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
t : Set ι := {i : ι | IsMulIndecomposable v {j : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v j) : S)} i}
s : Set ι := {j : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v j) : S) ∧ v j ∉ closure (v '' t)}
hne : s.Nonempty
obtain : ∀ (i : ι) (hi : MinimalFor.{u_1 + 1, u_4} (α := S) (fun (x : ι) ↦ x ∈ s) ((⇑f : (a : M) → S) ∘ v) i), False
⊢ False

Tactic:
obtain ⟨i, hi⟩ := s.toFinite.exists_minimalFor (f ∘ v) s hne

Premises used: Function.comp, Set.Finite.exists_minimalFor, Set.toFinite, DFunLike.coe
-- 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 : Finite ι
inst_3 : CommMonoid S
inst_4 : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
t : Set ι := {i : ι | IsMulIndecomposable v {j : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v j) : S)} i}
s : Set ι := {j : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v j) : S) ∧ v j ∉ closure (v '' t)}
hne : s.Nonempty
i : ι
hi : MinimalFor.{u_1 + 1, u_4} (α := S) (fun (x : ι) ↦ x ∈ s) ((⇑f : (a : M) → S) ∘ v) i
⊢ LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)

Tactic:
have ⟨(hi₀ : 1 < f (v i)), (hi₁ : v i ∉ _)⟩ : i ∈ s := hi.prop
-- 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 : Finite ι
inst_3 : CommMonoid S
inst_4 : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
t : Set ι := {i : ι | IsMulIndecomposable v {j : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v j) : S)} i}
s : Set ι := {j : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v j) : S) ∧ v j ∉ closure (v '' t)}
hne : s.Nonempty
i : ι
hi : MinimalFor.{u_1 + 1, u_4} (α := S) (fun (x : ι) ↦ x ∈ s) ((⇑f : (a : M) → S) ∘ v) i
hi₀ : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)
⊢ v i ∉ closure (v '' t)

Tactic:
have ⟨(hi₀ : 1 < f (v i)), (hi₁ : v i ∉ _)⟩ : i ∈ s := hi.prop
-- 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 : Finite ι
inst_3 : CommMonoid S
inst_4 : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
t : Set ι := {i : ι | IsMulIndecomposable v {j : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v j) : S)} i}
s : Set ι := {j : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v j) : S) ∧ v j ∉ closure (v '' t)}
hne : s.Nonempty
i : ι
hi : MinimalFor.{u_1 + 1, u_4} (α := S) (fun (x : ι) ↦ x ∈ s) ((⇑f : (a : M) → S) ∘ v) i
hi₀ : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)
hi₁ : v i ∉ closure (v '' t)
k : ι
hk₀ : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v k) : S)
hk₁ : LT.lt.{u_4} (α := S) ((f : (a : M) → S) (v k) : S) ((f : (a : M) → S) (v i) : S)
by_contra : ∀ (hk₂ : v k ∉ closure (v '' t)), False
⊢ Membership.mem (γ := Submonoid M) (closure (v '' t)) (v k)

Tactic:
by_contra hk₂
-- 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 : Finite ι
inst_3 : CommMonoid S
inst_4 : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
t : Set ι := {i : ι | IsMulIndecomposable v {j : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v j) : S)} i}
s : Set ι := {j : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v j) : S) ∧ v j ∉ closure (v '' t)}
hne : s.Nonempty
i : ι
hi : MinimalFor.{u_1 + 1, u_4} (α := S) (fun (x : ι) ↦ x ∈ s) ((⇑f : (a : M) → S) ∘ v) i
hi₀ : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)
hi₁ : v i ∉ closure (v '' t)
k : ι
hk₀ : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v k) : S)
hk₁ : LT.lt.{u_4} (α := S) ((f : (a : M) → S) (v k) : S) ((f : (a : M) → S) (v i) : S)
hk₂ : v k ∉ closure (v '' t)
⊢ False

Tactic:
not_le.mpr hk₁ <| hi.le_of_le ⟨hk₀, hk₂⟩ hk₁.le

Premises used: not_le, Iff.mpr, LT.lt.le, And.intro, MinimalFor.le_of_le
-- 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 : Finite ι
inst_3 : CommMonoid S
inst_4 : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
t : Set ι := {i : ι | IsMulIndecomposable v {j : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v j) : S)} i}
s : Set ι := {j : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v j) : S) ∧ v j ∉ closure (v '' t)}
hne : s.Nonempty
i : ι
hi : MinimalFor.{u_1 + 1, u_4} (α := S) (fun (x : ι) ↦ x ∈ s) ((⇑f : (a : M) → S) ∘ v) i
hi₀ : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)
hi₁ : v i ∉ closure (v '' t)
k : ι
hk₀ : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v k) : S)
hk₁ : LT.lt.{u_4} (α := S) ((f : (a : M) → S) (v k) : S) ((f : (a : M) → S) (v i) : S)
hk₂ : v k ∉ closure (v '' t)
⊢ False

Tactic:
exact not_le.mpr hk₁ <| hi.le_of_le ⟨hk₀, hk₂⟩ hk₁.le

Premises used: not_le, Iff.mpr, LT.lt.le, And.intro, MinimalFor.le_of_le
-- 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 : Finite ι
inst_3 : CommMonoid S
inst_4 : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
t : Set ι := {i : ι | IsMulIndecomposable v {j : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v j) : S)} i}
s : Set ι := {j : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v j) : S) ∧ v j ∉ closure (v '' t)}
hne : s.Nonempty
i : ι
hi : MinimalFor.{u_1 + 1, u_4} (α := S) (fun (x : ι) ↦ x ∈ s) ((⇑f : (a : M) → S) ∘ v) i
hi₀ : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)
hi₁ : v i ∉ closure (v '' t)
⊢ ∀ (k : ι) (hk₀ : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v k) : S))
    (hk₁ : LT.lt.{u_4} (α := S) ((f : (a : M) → S) (v k) : S) ((f : (a : M) → S) (v i) : S)),
    Membership.mem (γ := Submonoid M) (closure (v '' t)) (v k)

Tactic:
have hi₂ (k : ι) (hk₀ : 1 < f (v k)) (hk₁ : f (v k) < f (v i)) : v k ∈ closure (v '' t) := by
    by_contra hk₂; exact not_le.mpr hk₁ <| hi.le_of_le ⟨hk₀, hk₂⟩ hk₁.le
-- 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 : Finite ι
inst_3 : CommMonoid S
inst_4 : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
t : Set ι := {i : ι | IsMulIndecomposable v {j : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v j) : S)} i}
s : Set ι := {j : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v j) : S) ∧ v j ∉ closure (v '' t)}
hne : s.Nonempty
i : ι
hi : MinimalFor.{u_1 + 1, u_4} (α := S) (fun (x : ι) ↦ x ∈ s) ((⇑f : (a : M) → S) ∘ v) i
hi₀ : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)
hi₁ : v i ∉ closure (v '' t)
hi₂ :
  ∀ (k : ι) (hk₀ : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v k) : S))
    (hk₁ : LT.lt.{u_4} (α := S) ((f : (a : M) → S) (v k) : S) ((f : (a : M) → S) (v i) : S)),
    Membership.mem (γ := Submonoid M) (closure (v '' t)) (v k)
contrapose : ∀ (hi₁ : i ∈ t), Membership.mem (γ := Submonoid M) (closure (v '' t)) (v i)
⊢ i ∉ t

Tactic:
contrapose hi₁
-- 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 : Finite ι
inst_3 : CommMonoid S
inst_4 : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
t : Set ι := {i : ι | IsMulIndecomposable v {j : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v j) : S)} i}
s : Set ι := {j : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v j) : S) ∧ v j ∉ closure (v '' t)}
hne : s.Nonempty
i : ι
hi : MinimalFor.{u_1 + 1, u_4} (α := S) (fun (x : ι) ↦ x ∈ s) ((⇑f : (a : M) → S) ∘ v) i
hi₀ : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)
hi₂ :
  ∀ (k : ι) (hk₀ : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v k) : S))
    (hk₁ : LT.lt.{u_4} (α := S) ((f : (a : M) → S) (v k) : S) ((f : (a : M) → S) (v i) : S)),
    Membership.mem (γ := Submonoid M) (closure (v '' t)) (v k)
hi₁ : i ∈ t
⊢ Membership.mem (γ := Submonoid M) (closure (v '' t)) (v i)

Tactic:
subset_closure <| mem_image_of_mem v hi₁

Premises used: Set.mem_image_of_mem, Submonoid.subset_closure
-- 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 : Finite ι
inst_3 : CommMonoid S
inst_4 : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
t : Set ι := {i : ι | IsMulIndecomposable v {j : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v j) : S)} i}
s : Set ι := {j : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v j) : S) ∧ v j ∉ closure (v '' t)}
hne : s.Nonempty
i : ι
hi : MinimalFor.{u_1 + 1, u_4} (α := S) (fun (x : ι) ↦ x ∈ s) ((⇑f : (a : M) → S) ∘ v) i
hi₀ : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)
hi₂ :
  ∀ (k : ι) (hk₀ : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v k) : S))
    (hk₁ : LT.lt.{u_4} (α := S) ((f : (a : M) → S) (v k) : S) ((f : (a : M) → S) (v i) : S)),
    Membership.mem (γ := Submonoid M) (closure (v '' t)) (v k)
hi₁ : i ∈ t
⊢ Membership.mem (γ := Submonoid M) (closure (v '' t)) (v i)

Tactic:
exact subset_closure <| mem_image_of_mem v hi₁

Premises used: Set.mem_image_of_mem, Submonoid.subset_closure
-- 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 : Finite ι
inst_3 : CommMonoid S
inst_4 : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
t : Set ι := {i : ι | IsMulIndecomposable v {j : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v j) : S)} i}
s : Set ι := {j : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v j) : S) ∧ v j ∉ closure (v '' t)}
hne : s.Nonempty
i : ι
hi : MinimalFor.{u_1 + 1, u_4} (α := S) (fun (x : ι) ↦ x ∈ s) ((⇑f : (a : M) → S) ∘ v) i
hi₀ : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)
hi₁ : v i ∉ closure (v '' t)
hi₂ :
  ∀ (k : ι) (hk₀ : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v k) : S))
    (hk₁ : LT.lt.{u_4} (α := S) ((f : (a : M) → S) (v k) : S) ((f : (a : M) → S) (v i) : S)),
    Membership.mem (γ := Submonoid M) (closure (v '' t)) (v k)
⊢ i ∉ t

Tactic:
have hi₃ : i ∉ t := by contrapose hi₁; exact subset_closure <| mem_image_of_mem v hi₁
-- 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 : Finite ι
inst_3 : CommMonoid S
inst_4 : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
t : Set ι := {i : ι | IsMulIndecomposable v {j : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v j) : S)} i}
s : Set ι := {j : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v j) : S) ∧ v j ∉ closure (v '' t)}
hne : s.Nonempty
i : ι
hi : MinimalFor.{u_1 + 1, u_4} (α := S) (fun (x : ι) ↦ x ∈ s) ((⇑f : (a : M) → S) ∘ v) i
hi₀ : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)
hi₁ : v i ∉ closure (v '' t)
hi₂ :
  ∀ (k : ι) (hk₀ : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v k) : S))
    (hk₁ : LT.lt.{u_4} (α := S) ((f : (a : M) → S) (v k) : S) ((f : (a : M) → S) (v i) : S)),
    Membership.mem (γ := Submonoid M) (closure (v '' t)) (v k)
hi₃ : i ∉ t
⊢ ∃ (j : ι) (k : ι) (_ : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v j) : S)) (_ :
    LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v k) : S)), v i = v j * v k

Tactic:
grind [IsMulIndecomposable]

Premises used: IsMulIndecomposable
-- 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 : Finite ι
inst_3 : CommMonoid S
inst_4 : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
t : Set ι := {i : ι | IsMulIndecomposable v {j : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v j) : S)} i}
s : Set ι := {j : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v j) : S) ∧ v j ∉ closure (v '' t)}
hne : s.Nonempty
i : ι
hi : MinimalFor.{u_1 + 1, u_4} (α := S) (fun (x : ι) ↦ x ∈ s) ((⇑f : (a : M) → S) ∘ v) i
hi₀ : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)
hi₁ : v i ∉ closure (v '' t)
hi₂ :
  ∀ (k : ι) (hk₀ : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v k) : S))
    (hk₁ : LT.lt.{u_4} (α := S) ((f : (a : M) → S) (v k) : S) ((f : (a : M) → S) (v i) : S)),
    Membership.mem (γ := Submonoid M) (closure (v '' t)) (v k)
hi₃ : i ∉ t
obtain :
  ∀ (j k : ι) (hj : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v j) : S))
    (hk : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v k) : S)) (hjk : v i = v j * v k), False
⊢ False

Tactic:
obtain ⟨j, k, hj, hk, hjk⟩ : ∃ (j k : ι) (hj : 1 < f (v j)) (hk : 1 < f (v k)),
      v i = v j * v k := by
    grind [IsMulIndecomposable]
-- 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 : Finite ι
inst_3 : CommMonoid S
inst_4 : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
t : Set ι := {i : ι | IsMulIndecomposable v {j : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v j) : S)} i}
s : Set ι := {j : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v j) : S) ∧ v j ∉ closure (v '' t)}
hne : s.Nonempty
i : ι
hi : MinimalFor.{u_1 + 1, u_4} (α := S) (fun (x : ι) ↦ x ∈ s) ((⇑f : (a : M) → S) ∘ v) i
hi₀ : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)
hi₁ : v i ∉ closure (v '' t)
hi₂ :
  ∀ (k : ι) (hk₀ : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v k) : S))
    (hk₁ : LT.lt.{u_4} (α := S) ((f : (a : M) → S) (v k) : S) ((f : (a : M) → S) (v i) : S)),
    Membership.mem (γ := Submonoid M) (closure (v '' t)) (v k)
hi₃ : i ∉ t
j k : ι
hj : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v j) : S)
hk : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v k) : S)
hjk : v i = v j * v k
⊢ LT.lt.{u_4} (α := S) ((f : (a : M) → S) (v j) : S) ((f : (a : M) → S) (v i) : S)

Tactic:
aesop
-- 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 : Finite ι
inst_3 : CommMonoid S
inst_4 : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
t : Set ι := {i : ι | IsMulIndecomposable v {j : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v j) : S)} i}
s : Set ι := {j : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v j) : S) ∧ v j ∉ closure (v '' t)}
hne : s.Nonempty
i : ι
hi : MinimalFor.{u_1 + 1, u_4} (α := S) (fun (x : ι) ↦ x ∈ s) ((⇑f : (a : M) → S) ∘ v) i
hi₀ : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)
hi₁ : v i ∉ closure (v '' t)
hi₂ :
  ∀ (k : ι) (hk₀ : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v k) : S))
    (hk₁ : LT.lt.{u_4} (α := S) ((f : (a : M) → S) (v k) : S) ((f : (a : M) → S) (v i) : S)),
    Membership.mem (γ := Submonoid M) (closure (v '' t)) (v k)
hi₃ : i ∉ t
j k : ι
hj : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v j) : S)
hk : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v k) : S)
hjk : v i = v j * v k
⊢ Membership.mem (γ := Submonoid M) (closure (v '' t)) (v j)

Tactic:
have hj' : v j ∈ closure (v '' t) := hi₂ j hj <| by aesop
-- 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 : Finite ι
inst_3 : CommMonoid S
inst_4 : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
t : Set ι := {i : ι | IsMulIndecomposable v {j : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v j) : S)} i}
s : Set ι := {j : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v j) : S) ∧ v j ∉ closure (v '' t)}
hne : s.Nonempty
i : ι
hi : MinimalFor.{u_1 + 1, u_4} (α := S) (fun (x : ι) ↦ x ∈ s) ((⇑f : (a : M) → S) ∘ v) i
hi₀ : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)
hi₁ : v i ∉ closure (v '' t)
hi₂ :
  ∀ (k : ι) (hk₀ : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v k) : S))
    (hk₁ : LT.lt.{u_4} (α := S) ((f : (a : M) → S) (v k) : S) ((f : (a : M) → S) (v i) : S)),
    Membership.mem (γ := Submonoid M) (closure (v '' t)) (v k)
hi₃ : i ∉ t
j k : ι
hj : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v j) : S)
hk : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v k) : S)
hjk : v i = v j * v k
hj' : Membership.mem (γ := Submonoid M) (closure (v '' t)) (v j)
⊢ LT.lt.{u_4} (α := S) ((f : (a : M) → S) (v k) : S) ((f : (a : M) → S) (v i) : S)

Tactic:
aesop
-- 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 : Finite ι
inst_3 : CommMonoid S
inst_4 : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
t : Set ι := {i : ι | IsMulIndecomposable v {j : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v j) : S)} i}
s : Set ι := {j : ι | LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v j) : S) ∧ v j ∉ closure (v '' t)}
hne : s.Nonempty
i : ι
hi : MinimalFor.{u_1 + 1, u_4} (α := S) (fun (x : ι) ↦ x ∈ s) ((⇑f : (a : M) → S) ∘ v) i
hi₀ : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v i) : S)
hi₁ : v i ∉ closure (v '' t)
hi₂ :
  ∀ (k : ι) (hk₀ : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v k) : S))
    (hk₁ : LT.lt.{u_4} (α := S) ((f : (a : M) → S) (v k) : S) ((f : (a : M) → S) (v i) : S)),
    Membership.mem (γ := Submonoid M) (closure (v '' t)) (v k)
hi₃ : i ∉ t
j k : ι
hj : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v j) : S)
hk : LT.lt.{u_4} (α := S) (1 : S) ((f : (a : M) → S) (v k) : S)
hjk : v i = v j * v k
hj' : Membership.mem (γ := Submonoid M) (closure (v '' t)) (v j)
⊢ Membership.mem (γ := Submonoid M) (closure (v '' t)) (v k)

Tactic:
have hk' : v k ∈ closure (v '' t) := hi₂ k hk <| by aesop